Type Reconstruction with First-Class Polymorphic Values

We present the rst 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 rst-class polymorphic values. We accomplish this exibility by providing both generic and explicitly-quanti ed 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.

• Type: Conference
• Year: 1989
• Where: PLDI
• Authors: James O'Toole, David K. Gifford
• Keywords: PLDI 1989, Programming Languages, Rst Type Reconstruction, Type Reconstruction, Type Reconstruction Algorithm