Putting Type Annotations to Work

Martin Odersky and Konstantin L"aufer

Proc. 23rd ACM Symposium on Principles of Programming Languages, January 1996

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.