Understanding Hindley–Milner

06 Jun, 2025

Disclaimer: Before starting, be warned this post is inspired by the video series Type Systems: Lambda calculus to Hindley-Milner by Adam Jones. I strongly recommend you watch this if you, like me, has been struggling to get into Hindley-Milner, and type theory in general.

Hindley-Milner is a type system for the lambda calculus. A type system is a set of rules for assigning types to expressions. They can verify that annotated types are correct, or infer the types. On the other hand, lambda calculus is a mathematical system created to reason about computation. Is like a really really small programming language.

The type system was originally described by J. Roger Hindley in 1969 for combinatory logic. Then, rediscovered by Robin Milner in 1978 for the ML programming language. Finally, Damas formalized the type system for lambda calculus in 1984.

The core value of Handley-Milner is to support generic programming while mostly not needing type annotations. With the Hindley-Milner system, the most general type for an expression can be inferred.

Most popular languages that use variations of this system include Haskell, OCaml, Rust, Swift, Elm and Gleam.

How this looks in practice?

The easiest way to implement a type system is to require type annotations, and then verify that incosistencies don't exist. The other easiest way to implement a type system it's to make the language sytanx directed. Meaning and integer literal always going to be an integer, unless stated otherwise.

This requires less type annotations, but some expressions will still need them to disambiguate. For example:

list = []
list.append(1)
list.append(2)
list.append(3)

Here, list needs a type annotation to know what type of list it is even though clearly its a list of integers.

In a Hindley-Milner type system, annotating the type of the list wouldn't be necessary. The type of list would be inferred based on how it is used. We can see that integers are appended after the declaration, so the list must be a list of integers.

This makes easy to write generic code and code that's easy to change, while maintaining static type safety. If you want to be explicit, you can always add type annotations later.

Formalization

Hindley-Milner consists of a set of rules about types in lambda calculus. Then, an algorithm can make use of these rules to infer types. That's the case for algorithm W and algorithm M.

Lambda calculus with let polymorphism (The language)

Its syntax can be described as:

\begin{matrix} e = & x \\ | & e_{1} e_{2} \\ | & λ x \to e \\ | & l e t x = e_{1} i n e_{2} \end{matrix}

An expression can be a variable/constant, an application, an anonymous function or a let expression. Some examples of expressions could be:

$o d d 3$
$λ x \to o d d x$
$(λ x \to x) 3$
$l e t i d e n t i t y = λ x \to x i n i d e n t i t y 10$

An application is just a function call.

On the other hand, the equivalent of a let expression in a modern programming language would be a function binding. This is what allows generic functions in a static type system.

\begin{matrix} (λ i d \to i d (o d d (i d 3))) (λ i d \to i d) \end{matrix}

The above expression would work well in an untyped programming language. But even if it makes sense, we could not infer the types correctly in a static type system for the previous expression. For this we must use a let expression.

\begin{matrix} l e t i d = λ i d \to i d i n i d (o d d (i d 3)) \end{matrix}

If we try to infer types for the function application, we first would find that the first argument of the identity function is an $i n t e g e r$ , and then a $b o o l e a n$ , this would be a type error. On the other hand, with let expression, we found first that type of $i d$ is $\forall t . t \to t$ . This means we can instantiate $i d$ separately in both function applications.

Types

\begin{matrix} τ = & α \\ | & C τ_{1} . . . τ_{n} \end{matrix}

A type can be a type variable or a type function application.

$C$ would be a constant type, like $I n t$ , $B o o l$ , $L i s t$ , $\to$ , etc. It can have any number of parameters.

Type schemes

\begin{matrix} σ = & τ \\ | & \forall α . σ \end{matrix}

A type scheme may consist of a type, or a a type quantified with for all. When an expression has a type with type variables, the for all ( $\forall$ ) allows you to instantiate the type variables every time the expression is used.

Type context

Is where you store what type different variables have. It's a list of variable to type assignments. Is denoted generally with $Γ$ .

Typing rules (The type system)

A typing rule consists of a premise and a conclusion. If the premise is true, then its conclusion also must be true. They are denoted like:

\begin{matrix} R u l e = \frac{P r e m i s e}{C o n c l u s i o n} \end{matrix}

The typing rules for Hindley-Milner are:

\begin{matrix} \frac{x : σ \in Γ}{Γ ⊢ x : σ} \end{matrix}

Variable typing rule: If assignment $x : σ$ is in $Γ$ then in context $Γ$ it follows that $x$ has type $σ$ .

\begin{matrix} \frac{Γ ⊢ e_{0} : τ_{a} \to τ_{b} Γ ⊢ e_{1} : τ_{a}}{Γ ⊢ e_{0} e_{1} : τ_{b}} \end{matrix}

Function application typing rule: If in context $Γ$ it follows that expression $e_{0}$ has type $τ_{a} \to τ_{b}$ and expression $e_{1}$ has type $τ_{a}$ . Then, in context $Γ$ it follows the expression $e_{0} e_{1}$ has type $τ_{b}$ .

\begin{matrix} \frac{Γ + x : τ_{a} ⊢ e : τ_{b}}{Γ ⊢ λ x \to e : τ_{a} \to τ_{b}} \end{matrix}

Function abstraction typing rule: If it follows that expression $e$ has type $τ_{b}$ in the case we add $x : τ_{a}$ to $Γ$ . Then, it follows that in $Γ$ the expression $λ x \to e$ has type $τ_{a} \to τ_{b}$ .

\begin{matrix} \frac{Γ ⊢ e_{0} : σ Γ + x : σ ⊢ e_{1} : τ}{Γ ⊢ l e t x = e_{0} i n e_{1} : τ} \end{matrix}

Let binding rule: If in $Γ$ it follows that $e_{0}$ has type $σ$ , and it follows that if we add $x : σ$ to typing context $e_{1}$ has type $τ$ . Then, it follows that the expression $l e t x = e_{0} i n e_{1}$ has type $τ$ .

Algorithm W (An inference algorithm)

The following is the first algorithm proposed to infer types in Hindlye-Milner types. It is a recursive algorithm that takes as input a type context and an expression, and returns a substitution and a type. The type is what we care about.

\begin{matrix} W (Γ, x) = & (i d e n t i t y, i n s t a n t i a t e (Γ (x))) \\ W (Γ, λ x \to e) = & l e t (S_{1}, τ_{b}) = W (Γ + x : n e w τ_{a}, e) \\ i n (S_{1}, S_{1} (τ_{a} \to τ_{b})) \\ W (Γ, e_{1} e_{2}) = & l e t \\ (S_{1}, τ_{1}) = W (Γ, e_{1}) \\ (S_{2}, τ_{a}) = W (Γ, e_{2}) \\ S_{3} = u n i f y (S_{2} (τ_{1}), τ_{a} \to n e w τ_{b}) \\ i n & (S_{3} S_{2} S_{1}, S_{3} τ_{b}) \\ W (Γ, l e t x = e_{1} i n e_{2}) = & l e t \\ (S_{1}, τ_{1}) = W (Γ, e_{1}) \\ (S_{2}, τ_{2}) = W (S_{1} Γ + x : g e n e r a l i z e (S_{1} Γ, τ_{1}), e_{2}) \\ i n (S_{2} S_{1}, τ_{2}) \end{matrix}

The function instantiate takes a type scheme, and for each for all creates a new type variable and replaces it in the body of the type. The result is a type without for all quantifiers.

The function unify takes two types and returns a substitution that, when applied to both types, makes them equal.

A substitution is a list of mappings from type variables to other types.

The function generalize adds for all quantifiers to free type variables in a type. i.e. it adds a for all quantifier to all type variables in a type that are not currently quantified.

Algorithm M (Another inference algorithm)

M is also a recursive algorithm, but it takes as input a type context, a expression, and a type, and returns a substitution. If we want to infer the type of an expression $e$ , we create a new type variable $τ$ and call $M (Γ, e, τ)$ . Then we apply the resulting substitution to $τ$ to know the type of $e$ .

\begin{matrix} M (Γ, x, τ) = & u n i f y (τ, i n s t a n t i a t e (Γ (x))) \\ M (Γ, λ x \to e, τ) = & l e t \\ S_{1} = u n i f y (τ, n e w τ_{a} \to n e w τ_{b}) \\ S_{2} = M (S_{1} Γ + x : S_{1} τ_{a}, e, S_{1} τ_{b}) \\ i n S_{2} S_{1} \\ M (Γ, e_{1} e_{2}, τ_{b}) = & l e t \\ S_{1} = M (Γ, e_{1}, n e w τ_{a} \to τ_{b}) \\ S_{2} = M (S_{1} Γ, e_{2}, S_{1} τ_{a}) \\ i n S_{2} S_{1} \\ M (Γ, l e t x = e_{1} i n e_{2}, τ) = & l e t \\ S_{1} = M (Γ, e_{1}, n e w τ_{1}) \\ S_{2} = M (S_{1} Γ + x : g e n e r a l i z e (S_{1} Γ, S_{1} τ_{1}), e_{2}, S_{1} τ) \\ i n S_{2} S_{1} \end{matrix}

Algorithm M is top-down instead of bottom-up. This means constraints are propagated from the top, and if we detect an error, we report it in a leaf.