HMF: Simple type inference for first-class polymorphism

HMF: Simple type inference for first-class polymorphism - Daan Leijen, Draft April 8, 2008.

HMF is a conservative extension of Hindley-Milner type inference with first-class polymorphism and regular System F types. The system
distinguishes itself from other proposals with simple type rules and a very simple type inference algorithm that is just a small extension
of the usual Damas-Milner algorithm. Given the relative simplicity and expressive power, we feel that HMF can be a very attractive
type system in practice. There is a reference implementation of the type system available at:

An excellent paper even in its current draft form. I also placed this under the learning category, because Daan's writing style is lucid enough that the concepts can be understood by relative newcomers to the field of type theory

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Very appealing

The type checking algorithm is relatively simple, the type system is familiar and predictable, and we have first-class polymorphism at the cost of a few type annotations. I hope this catches on (OCaml, I'm looking at you).