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

meaning that expression has type under type environment .

Object Language

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

Here:

• is a variable;
• is a constant with a predefined type;
• introduces a function;
• applies a function;
• let is the source of parametric polymorphism.

Types

Monotypes

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

Here:

• is a type variable;
• is a base type, such as or ;
• 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:

The scheme

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

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

Type Environments

A type environment maps term variables to type schemes:

For example:

A variable looked up from may be instantiated before use.

Free Type Variables

Let be the set of free type variables in :

For type schemes and environments:

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

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:

Only variables not already mentioned by may be generalised.

Instantiation

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

where are fresh.

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

Typing Rules

Variable

A variable is looked up and instantiated.

Constant

Constants are treated like predefined variables in a global environment .

Abstraction

The parameter is monomorphic inside the abstraction.

Application

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

Let

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

Inference Principle

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

where:

• is a type substitution;
• is the inferred monotype;
• if inference succeeds.

A type substitution maps type variables to types:

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

The occurs check rejects equations such as

because they would require an infinite type.

Principal Type Property

Principal type property

If an expression is typable in HM under , then there exists a monotype such that:

1. ;
2. for every with , there is a substitution with .

Thus is the most general type scheme for .

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:

First infer the bound expression:

Since , generalise:

In the body, each occurrence is instantiated separately:

Application requires

Unification gives

Therefore:

The whole expression has principal type scheme:

Boundary

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

• higher-rank polymorphism, where 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.