What is Hindley-Milner?

Question

I encountered this term Hindley-Milner, and I'm not sure if grasp what it means.

I've read the following posts:

• Steve Yegge - Dynamic Languages Strike Back
• Steve Yegge - The Pinocchio Problem
• Daniel Spiewak - What is Hindley-Milner? (and why is it cool?)

But there is no single entry for this term in wikipedia where usually offers me a concise explanation.
^{Note - one has now been added}

What is it?
What languages and tools implement or use it?
Would you please offer a concise answer?

Answer 1

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.