Putting Type Annotations to Work

We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix. 1 Introduction Two of the most important cornerstones of type theory for programming languages are the Hindley/Milner system and the second-order polymorphic -calculus. This paper tries to explore some of the design space between them. The Hindley/Milner system [Mil78] extends the simply-typed -calculus with polymorphic let-bound identifiers. It thus adds considerable expressive power yet retains the property that no type annotations in programs are needed, since most gen..