Type reconstruction with first-class polymorphic values
- 21 June 1989
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 24 (7) , 207-217
- https://doi.org/10.1145/74818.74836
Abstract
We present the first type reconstruction system which combines the implicit typing of ML with the full power of the explicitly typed second-order polymorphic lambda calculus. The system will accept ML-style programs, explicitly typed programs, and programs that use explicit types for all first-class polymorphic values. We accomplish this flexibility by providing both generic and explicitly-quantified polymorphic types, as well as operators which convert between these two forms of polymorphism. This type reconstruction system is an integral part of the FX-89 programming language. We present a type reconstruction algorithm for the system. The type reconstruction algorithm is proven sound and complete with respect to the formal typing rules.Keywords
This publication has 9 references indexed in Scilit:
- A theory of type polymorphism in programmingPublished by Elsevier ,2003
- A proper extension of ML with an effective type-assignmentPublished by Association for Computing Machinery (ACM) ,1988
- Partial polymorphic type inference and higher-order unificationPublished by Association for Computing Machinery (ACM) ,1988
- Modules for standard MLPublished by Association for Computing Machinery (ACM) ,1984
- The typechecking of programs with implicit type structurePublished by Springer Nature ,1984
- The Expressiveness of Simple and Second-Order Type StructuresJournal of the ACM, 1983
- Polymorphic type inferencePublished by Association for Computing Machinery (ACM) ,1983
- Principal type-schemes for functional programsPublished by Association for Computing Machinery (ACM) ,1982
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965