Lambda the Ultimate

A recent enlightening discussion on recursive type inference at comp.lang.functional brought the following tutorial paper on ML type inference to my attention.

A modern eye on ML Type Inference by Francois Pottier INRIA September 2005.

Hindley and Milner’s type system is at the heart of programming languages such as Standard ML, Objective Caml, and Haskell. Its expressive power, as well the existence of a type inference algorithm, have made it quite successful. Traditional presentations of this algorithm, such as Milner’s Algorithm W, are somewhat obscure. These short lecture notes, written for the APPSEM’05 summer school, begin with a presentation of a more modern, constraint-based specification of the algorithm, and explain how it can be extended to accommodate features such as algebraic data types, recursion, and (lexically scoped) type annotations. Then, two chapters, yet to be written, review two recent proposals for incorporating more advanced features, known as arbitrary-rank predicative polymorphism and generalized algebraic data types. These proposals combine a traditional constraint-based type inference algorithm with a measure of local type inference.