Type-Reconstruction wit First-Class Polymorphic Values

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 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 atype reconstruction algorithm for the system. The type reconstruction algorithm is proven sound and complete with respect to the formal typing rules