Hindley–Milner Type System

type-theory

Definition

Hindley–Milner Type System

The Hindley–Milner type system is a static type system for a lambda calculus with let, where every typable expression has a principal type scheme and where type inference is decidable by unification.

Its central judgement has the form

$$\Gamma ⊢e:\tau ,$$

meaning that expression $e$ has type $\tau$ under type environment $\Gamma$.

Object Language

HM is usually presented over the simply typed lambda calculus extended with let:

$$e::=x\mid c\mid \lambda x.e\mid e_1{e}_2\mid \mathbf{let}x=e_1\mathbf{in}{e}_2.$$

Here:

• $x\in \mathcal{V}$ is a variable;
• $c\in \mathcal{C}$ is a constant with a predefined type;
• $\lambda x.e$ introduces a function;
• $e_1{e}_2$ applies a function;
• let is the source of parametric polymorphism.

Types

Monotypes

A monotype is an ordinary type with no explicit universal quantifier:

$$\tau ::=\alpha \mid b\mid {\tau }_1\to {\tau }_2.$$

Here:

• $\alpha \in \mathcal{A}$ is a type variable;
• $b\in \mathcal{B}$ is a base type, such as $\mathrm{Int}$ or $\mathrm{Bool}$;
• ${\tau }_1\to {\tau }_2$ is a function type.

Extensions often add product types, sum types, lists, records, and algebraic data types, but the core mechanism does not require them.

Type Schemes

A type scheme is a type with universal quantification over some type variables:

$$\sigma ::=\forall {\alpha }_1\dots {\alpha }_n.\tau .$$

The scheme

$$\forall \alpha .\alpha \to \alpha$$

means: for every type $\alpha$, the expression may be used as a function from $\alpha$ to $\alpha$.

HM is rank-1 polymorphic: universal quantifiers appear only at the outermost level of type schemes stored in $\Gamma$.

Type Environments

A type environment maps term variables to type schemes:

$$\Gamma :\mathcal{V}\rightharpoonup \Sigma .$$

For example:

$$\Gamma =\{\mathrm{id}:\forall \alpha .\alpha \to \alpha ,n:\mathrm{Int}\}.$$

A variable looked up from $\Gamma$ may be instantiated before use.

Free Type Variables

Let $\mathrm{ftv}(\tau )$ be the set of free type variables in $\tau$:

$$\begin{array}{rl}\mathrm{ftv}(\alpha )& =\{\alpha \},\\ \mathrm{ftv}(b)& =\varnothing ,\\ \mathrm{ftv}({\tau }_1\to {\tau }_2)& =\mathrm{ftv}({\tau }_1)\cup \mathrm{ftv}({\tau }_2).\end{array}$$

For type schemes and environments:

$$\begin{array}{rl}\mathrm{ftv}(\forall {\alpha }_1\dots {\alpha }_n.\tau )& =\mathrm{ftv}(\tau )\setminus \{{\alpha }_1,\dots ,{\alpha }_n\},\\ \mathrm{ftv}(\Gamma )& =\bigcup _{x:\sigma \in \Gamma }\mathrm{ftv}(\sigma ).\end{array}$$

Free type variables are exactly the type variables that are not locally bound by a $\forall$.

Generalisation and Instantiation

HM has two complementary operations.

Generalisation

After inferring a type for a let-bound expression, HM quantifies over type variables that are not fixed by the surrounding environment:

$$\mathrm{gen}(\Gamma ,\tau )=\forall \overline{\alpha }.\tau \text{where}\overline{\alpha }=\mathrm{ftv}(\tau )\setminus \mathrm{ftv}(\Gamma ).$$

Only variables not already mentioned by $\Gamma$ may be generalised.

Instantiation

When a polymorphic variable is used, HM replaces its quantified variables by fresh type variables:

$$\mathrm{inst}(\forall {\alpha }_1\dots {\alpha }_n.\tau )=\tau [{\beta }_1/{\alpha }_1,\dots ,{\beta }_n/{\alpha }_n],$$

where ${\beta }_1,\dots ,{\beta }_n$ are fresh.

Thus each use of a let-bound polymorphic variable receives its own copy of the type.

Typing Rules

Variable

$$\frac{x:\sigma \in \Gamma \tau =\mathrm{inst}(\sigma )}{\Gamma ⊢x:\tau }{}_{\text{(var)}}$$

A variable is looked up and instantiated.

Constant

$$\frac{c:\sigma \in {\Gamma }_0\tau =\mathrm{inst}(\sigma )}{\Gamma ⊢c:\tau }{}_{\text{(const)}}$$

Constants are treated like predefined variables in a global environment ${\Gamma }_0$.

Abstraction

$$\frac{\Gamma ,x:{\tau }_1⊢e:{\tau }_2}{\Gamma ⊢\lambda x.e:{\tau }_1\to {\tau }_2}{}_{\text{(abs)}}$$

The parameter $x$ is monomorphic inside the abstraction.

Application

$$\frac{\Gamma ⊢e_1:{\tau }_1\to {\tau }_2\Gamma ⊢e_2:{\tau }_1}{\Gamma ⊢e_1{e}_2:{\tau }_2}{}_{\text{(app)}}$$

Application forces the function input type to match the argument type.

Let

$$\frac{\Gamma ⊢e_1:{\tau }_1\Gamma ,x:\mathrm{gen}(\Gamma ,{\tau }_1)⊢e_2:{\tau }_2}{\Gamma ⊢\mathbf{let}x=e_1\mathbf{in}{e}_2:{\tau }_2}{}_{\text{(let)}}$$

This is the key HM rule: infer $e_1$, generalise it, then type $e_2$ with $x$ available polymorphically.

Inference Principle

Algorithm W is a standard inference algorithm for HM. It computes either failure or a pair

$$W(\Gamma ,e)=(S,\tau ),$$

where:

• $S$ is a type substitution;
• $\tau$ is the inferred monotype;
• $S\Gamma ⊢e:\tau$ if inference succeeds.

A type substitution maps type variables to types:

$$S:\mathcal{A}\rightharpoonup \mathcal{T}.$$

For application, inference creates a fresh type variable and solves the equality constraint by a most general unifier:

$$\begin{array}{rl}W(\Gamma ,e_1)& =(S_1,{\tau }_1),\\ W(S_1\Gamma ,e_2)& =(S_2,{\tau }_2),\\ U& =\mathrm{mgu}(S_2{\tau }_1,{\tau }_2\to \alpha ),\\ W(\Gamma ,e_1{e}_2)& =(U\circ S_2\circ S_1,U\alpha ).\end{array}$$

The occurs check rejects equations such as

$$\alpha =\alpha \to \beta ,$$

because they would require an infinite type.

Principal Type Property

Principal type property

If an expression $e$ is typable in HM under $\Gamma$, then there exists a monotype ${\tau }_0$ such that:

1. $\Gamma ⊢e:{\tau }_0$;
2. for every $\tau$ with $\Gamma ⊢e:\tau$, there is a substitution $S$ with $S{\tau }_0=\tau$.

Thus $\mathrm{gen}(\Gamma ,{\tau }_0)$ is the most general type scheme for $e$.

The principal type property is what makes annotation-free inference practical: the system does not have to guess among unrelated valid types.[^damas-milner]

Worked Example

Consider:

$$\mathbf{let}\mathrm{id}=\lambda x.x\mathbf{in}\mathrm{id}\mathrm{id}.$$

First infer the bound expression:

$$\begin{array}{rl}x& :\alpha ,\\ \lambda x.x& :\alpha \to \alpha .\end{array}$$

Since $\alpha \notin \mathrm{ftv}(\varnothing )$, generalise:

$$\mathrm{id}:\forall \alpha .\alpha \to \alpha .$$

In the body, each occurrence is instantiated separately:

$$\begin{array}{rl}{\mathrm{id}}_1& :\beta \to \beta ,\\ {\mathrm{id}}_2& :\gamma \to \gamma .\end{array}$$

Application requires

$$\beta \to \beta =(\gamma \to \gamma )\to \delta .$$

Unification gives

$$\beta =\gamma \to \gamma ,\delta =\gamma \to \gamma .$$

Therefore:

$$\mathbf{let}\mathrm{id}=\lambda x.x\mathbf{in}\mathrm{id}\mathrm{id}:\gamma \to \gamma .$$

The whole expression has principal type scheme:

$$\forall \gamma .\gamma \to \gamma .$$

Boundary

HM is deliberately small. In its classical form it excludes:

• higher-rank polymorphism, where $\forall$ appears inside function arguments;
• ad-hoc overloading, unless added by a separate mechanism such as type classes;
• general subtyping;
• unrestricted polymorphic recursion;
• dependent types.

These features can be added to programming languages, but usually at the cost of a simpler principal-type theorem, complete inference, or both.