Abstract
Because of the ease of use and the versatility of widening operators, there seem to be good candidates for defining new type inference strategy wherever the type inference problem is not decidable.
More precisely, in this paper, we exhibit some widening operators that either mimic some type inference strategy that are already implemented in some languages, or extend the ML-type system. In fact, those widening operators are only selected operators from a much larger family of widening operators listed on figure 3 that works very well on the ML-type algebra.
But widening operators can be used to solve other problems than the termination of the ML+type inference problem. For example, in [7] we have introduced a new type algebra called Fractional Types. Since the intersection of two fractional types is not computable in some cases, we have to use a widening operator to compute a lower approximation of the intersection of two fractional types, and to ensure algorithm termination.
We intend to develop the widening techniques presented in this paper:
-
to search for sharper widening than those realized de facto by specific known algorithms, not only in ML, but wherever type inference is possible;
-
to bridge the gap between type inference and abstract interpretation techniques.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Aiken, B. Murphy, Static Type Inference in a Dynamically Typed Language, Conf. rec of the 18th ACM Symposium on POPL, Orlando Florida 279–290, Jan 1991.
M.Coppo, M.Dezani-Ciancaglini, An extension of the Basic Functionality Theory for the l-Calculus, Notre Dame, Journal of Formal Logic 21 (4), 1980.
P. Cousot, Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes. Thèse d'Etat, Grenoble 1978.
P. & R. Cousot, Abstract Interpretation: a unified lattice model for static analysis of program by construction of approximate fixpoints, Conf. rec of the 4th ACM Symposium on POPL, Jan 1977.
R. Harper, D. MacQueen, R. Milner Standard ML Report ECS-LFCS-86-2, Edinburgh University.
B. Monsuez Polymorphic Typing by Abstract Interpretation Conf. rec. of the 12th Conference on FST&TCS, December 1992, New Dehli, India, LNCS 652 Springer Verlag.
B. Monsuez Fractional Types Prooceding of the Workshop on Static Analysis, Septembre 1992, Bordeaux, France, BIGRE 82.
N.D. Jones, A. Mycroft, A relational framework for abstract interpretation in ”Program as Data Objects” Proc. of a workshop in Copenhagen Oct. 1985. Ed. Ganziger and Jones. LNCS 215 Springer Verlag.
T. Karnomori, K. Horiuchi Polymorphic Type Inference in Prolog by Abstract Interpretation, in Logic Programming '87, Tokyo, LNCS 315, 1988, 195–214.
A.J. Kfoury, J. Tiuryn, P. Urzyczyn, The undecidability of the semi-unification problem Proc. ACM Symp. Theory of Computing, 1990.
A. Mycroft Polymorphic Types Schemes and Recursive Definitions in LNCS 167 International Symposium on Programming. 6th Colloquium April 1984, Toulouse.
D. Turner, Miranda, a non-strict functional language with polymorphic types in Functional programming Languages and Computer Architecture, Nancy, LNCS 201.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Monsuez, B. (1993). Polymorphic types and widening operators. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds) Static Analysis. WSA 1993. Lecture Notes in Computer Science, vol 724. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57264-3_47
Download citation
DOI: https://doi.org/10.1007/3-540-57264-3_47
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57264-0
Online ISBN: 978-3-540-48027-3
eBook Packages: Springer Book Archive