Understanding Hindley–Milner

06 Jun, 2025

Before starting, be warned this post is heavily 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, have been struggling to get into Hindley-Milner, and type theory in general.

Having said that, 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 serve to verify that annotated types are correct or to infer the types. As for lambda calculus, is a mathematical system created to reason about computation. You can think of it as a very, very small programming language.

The Hindley-Milner 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 Hindley-Milner is to support generic programming while mostly not needing type annotations. In a Hindley-Milner type 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 inconsistencies don't exist. The other easiest way to implement a type system it's to make the language syntax directed. Syntax directed means that the type of any expressions can be derived just by looking a it. This requires less type annotations, but some expressions will still need them. 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 we can see it's 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.

The awesome things about Hindley-Milner type systems is that they make easy writing generic code and code that's easy to change while maintaining static type safety. And if you want to be explicit, you can always add type annotations later.

Formalization

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

Lambda calculus: 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 are:

$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 there exists an error, we found it in a leaf.