The Hindley-Milner Algorithm is an algorithm for determining the types of expressions. Basically it’s a formalisation of this earlier post. There’s an article on Wikipedia which is frustratingly terse and mathematical. This is my attempt to explain some of that article to myself, and to anyone else who may be interested.

### Background

The Hindley-Milner algorithm is concerned with type checking the lambda calculus, not any arbitrary programming language. However most (all?) programming language constructs can be transformed into lambda calculus. For example the lambda calculus only allows variables as formal arguments to functions, but the declaration of a temp variable:

1 2 3 4 |
{ var x = 10; // code that uses x } |

can be replaced by an anonymous function call with argument:

1 2 3 4 5 |
{ fn(x) { // code that uses x }(10); } |

Similarily the lambda calculus only treats on functions of one argument, but a function of more than one argument can be curried, etc.

### Expressions

We start by defining the expressions (e) we will be type-checking:

e | ::= | E | A primitive expression, i.e. 3. |

| | s | A symbol. | |

| | λs.e | A function definition. s is the formal argument symbol and e is the function body (expression). | |

| | (e e) | The application of an expression to an expression (a function call). |

### Types

Next we define our types (τ):

τ | ::= | T | A primitive type, i.e. `int` . |

| | τ_{0} → τ_{1} | A function of one argument taking type τ_{0} and returning type τ_{1} |

### Requirement

We need a function:

[1] | f(ε, e) | = | τ |

where:

ε | A type environment. |

e | An expression. |

τ | A type |

### Assumptions

We assume we already have:

[2] | f(ε, E) | = | T | A set of mappings from primitive expressions to their primitive types (from 3 to `int` , for example.) |

The following equations are logic equations. They are easy enough to read, Everything above the line are assumptions. The statement below the line should follow if the assumptions are true.

Our second assumption is:

[3] | (s, τ) | ∈ | ε | If (s, τ) is in ε (i.e. if ε has a mapping from s to τ) |

f(ε, s) | = | τ | Then in the context of ε, s is a τ |

Informally symbols are looked up in the type environment

.

### Deductions

[4] | f(ε, g) | = | τ_{1} → τ | If g is a function mapping a τ_{1} to a τ |

f(ε, e) | = | τ_{1} | and e is a τ_{1} | |

f(ε, (g e)) | = | τ | Then the application of g to e is a τ |

That is just common sense.

[5] | ε_{1} | = | ε ∪ (s, τ) | If ε_{1} is ε extended by (s, τ), e.g. if s is a τ |

f(ε, λs.e) | = | τ → f(ε_{1}, e) | Then the output type of a function with argument s of type τ, and body e, is the type of the body e in the context of ε_{1} |

This is just a bit tricky. We don’t necessarily know the value of τ when evaluating this expression, but that’s what logic variables are for.

### Algorithm

- We extend the set T of primitive types with an infinite set of type variables α
_{1}, α_{2}etc. - We have a function
`new`

which returns a fresh type variable each time it is called. - We have a function
`eq`

which unifies two equations.

We modify our function, part [4] (function application) as follows:

[6] | τ_{0} | = | f(ε, e_{0}) | If τ_{0} is the type of e_{0} |

τ_{1} | = | f(ε, e_{1}) | and τ_{1} is the type of e_{1} | |

τ | = | `new` | and τ is a fresh type variable | |

f(ε, (e0 e1)) | = | eq(τ_{0}, τ_{1} → τ); τ | Then after unifying τ_{0} with τ_{1} → τ, the type of (e_{0} e_{1}) is τ. |

That deserves a bit of discussion. We know e_{0} is a function, so it must have a type τ_{a} → τ_{b} for some types τ_{a} and τ_{b}. We calculate τ_{0} as the provisional type of e_{0} and τ_{1} as the type of e_{1}, then create a new type variable τ to hold the type of (e_{0} e_{1}).

### Problem

Suppose e_{0} is the function `length`

(the length of a list of some unspecified type τ_{2}), then τ_{0} should come out as [τ_{2}] → `int`

(using [x] to mean list of x

.)

Suppose further that τ_{1} is `char`

.

We therefore unify:

[τ_{2}] | → | `int` | ||

[`char` ] | → | τ |

Which correctly infers that the type of `(length [‘c’])`

is `int`

. Unfortunately, in doing so, we permanently unify τ_{2} with `char`

, forcing `length`

to have permanent type `[char]`

→ `int`

so this algorithm does not cope with polymorphic functions such as `length`

.