What is Hindley-Milner?

Hindley-Milner is a type system discovered independently by Roger Hindley (who was looking at logic) and later by Robin Milner (who was looking at programming languages). The advantages of Hindley-Milner are

• It supports polymorphic functions; for example, a function that can give you the length of the list independent of the type of the elements, or a function does a binary-tree lookup independent of the type of keys stored in the tree.

• Sometimes a function or value can have more than one type, as in the example of the length function: it can be "list of integers to integer", "list of strings to integer", "list of pairs to integer", and so on. In this case, a signal advantage of the Hindley-Milner system is that each well-typed term has a unique "best" type, which is called the principal type. The principal type of the list-length function is "for any a, function from list of a to integer". Here a is a so-called "type parameter," which is explicit in lambda calculus but implicit in most programming languages. The use of type parameters explains why Hindley-Milner is a system that implements parametric polymorphism. (If you write a definition of the length function in ML, you can see the type parameter thus:

   fun 'a length []      = 0
     | 'a length (x::xs) = 1 + length xs
  

• If a term has a Hindley-Milner type, then the principal type can be inferred without requiring any type declarations or other annotations by the programmer. (This is a mixed blessing, as anyone can attest who has ever been handled a large chunk of ML code with no annotations.)

Hindley-Milner is the basis for the type system of almost every statically typed functional language. Such languages in common use include

• The ML family (Standard ML and Objective Caml)
• Haskell
• Clean

All these languages have extended Hindley-Milner; Haskell, Clean, and Objective Caml do so in ambitious and unusual ways. (Extensions are required to deal with mutable variables, since basic Hindley-Milner can be subverted using, for example, a mutable cell holding a list of values of unspecified type. Such problems are dealt with by an extension called the value restriction.)

Many other minor languages and tools based on typed functional languages use Hindley-Milner.

Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.

You may be able to find the original papers using Google Scholar or CiteSeer -- or your local university library. The first is old enough that you may have to find bound copies of the journal, I couldn't find it online. The link that I found for the other one was broken, but there might be others. You'll certainly be able to find papers that cite these.

Hindley, Roger J, The principal type scheme of an object in combinatory logic, Transactions of the American Mathematical Society, 1969.

Milner, Robin, A Theory of Type Polymorphism, Journal of Computer and System Sciences, 1978.