Type Reconstruction with First-Class Polymorphic Values
MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE
Pagination or Media Count:
We present the first type reconstruction system which combines the implicit typing of ML with the full power of the explicity typed second-order polymorphic lambda calculus. The system will accept ML-style programs, explicity 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.
- Computer Programming and Software