Hindley-Milner

Hindley–Milner is a type system for the λ-calculus with parametric polymorphism. It has two key properties:

It can infer types without annotations.
It computes a principal type: the most general type from which all other valid types follow by specialization. ([Wikipedia]¹)

HM Types

We distinguish:

Monotypes (τ)

Monotypes (simple types) are built from:

Type constants: Int, Bool, String, …
Type variables: α, β, γ, …
Type constructors: function, lists, pairs, etc.

Typical grammar:

τ ::= α
    | Int | Bool | ...
    | τ -> τ
    | List τ
    | τ × τ         -- pairs, etc.

Polytypes / type schemes (σ)

Polytypes (type schemes) allow universal quantification over type variables:

σ ::= τ
    | ∀α. σ      -- usually written ∀α₁…αₙ. τ

Example:

∀α. α -> α is the type of the polymorphic identity function.
Int -> Int is a monomorphic specialization of that scheme.

In the environment Γ, variables map to schemes (polytypes), not bare monotypes. ([Wikipedia]¹)

Type Variables

During inference: Unknowns

When you don’t yet know the type of something, you introduce a fresh type variable:

For λx. x:
- Give x a fresh type α.
- The body x also has type α.
- The function has type α -> α.

At this stage, α is an inference variable: a placeholder to be solved later.

After Generalization: Parameters of a scheme

At a let, HM generalizes a monotype into a scheme by quantifying over its free type variables that aren’t pinned down by the environment:

Gen(Γ, τ) = ∀α₁…αₙ. τ
  where {αᵢ} = free(τ) \ free(Γ)

Example:

let id = λx. x in ...

Infer id : α -> α.
Generalization yields id : ∀α. α -> α.

Now α is a bound type variable in the scheme, exactly like a λ-bound term variable: it has scope within the body of the type.

When you use id, you:

Instantiate ∀α. α -> α to, say, β -> β with a fresh β.
Later unification may force β = Int, β = Bool, etc.

So:

Inference variables: “unknowns we’re solving for”.
Quantified variables: “parameters of a polymorphic function”.

Constraints and “Bounds” on Type Variables

Bound v. Free

A type variable is bound if it appears under a ∀:

In ∀α. α -> α, α is bound.
In ∀α. α -> β, α is bound, β is free.

Generalization at let takes free inference variables and turns them into bound quantified parameters.

This is purely syntactic, like “bound vs free variables” in λ-calculus.

Semantic Bounds: restricted instantiations (constrained HM)

Basic HM only has equality constraints between types (unification). But real languages often add an extra layer: constrained polymorphism, which you can think of as “bounds on type variables”.

Type schemes become:

∀α₁…αₙ. C ⇒ τ

where C is a set of constraints on the type variables—e.g. Eq α, Num α. This is the HM(X) framework: HM plus a parametric constraint system X that’s solved alongside unification. ([Tufts Computer Science]²)

Example (Haskell style):

show :: Show a => a -> String

Read as:

∀a. Show a ⇒ a -> String

Here a is:

Bound by ∀a.
Semantically bounded by the predicate Show a: you can only instantiate a with types that satisfy the Show constraint.

So:

Plain HM:
- Constraints are equations between types: τ₁ ~ τ₂.
- Bounds = “is this variable under a ∀?”. Unification just figures out equalities.
Constrained HM / HM(X):
- Constraints are logical predicates over types (Eq α, Num α, record rows, effects, etc.).
- Bounds = “α must satisfy constraint C when instantiated”.

For your own LSP/typechecker, this is where you decide if you want:

A pure Damas–Milner ([EECS Berkeley]³) core (just unification constraints), or
A constrained layer (e.g. traits/typeclasses/effects) integrated via HM(X)-style rules.

Typing Rules

You can present HM via a judgment:

Γ ⊢ e : τ

with Γ mapping variables to schemes. The important rules (up to let) are:

Var: If x : σ ∈ Γ, then
- instantiate σ to monotype τ,
- conclude Γ ⊢ x : τ.
Abs (λ): For λx. e:
- give x a fresh type α,
- infer Γ, x:α ⊢ e : τ,
- result type is α -> τ.
App (application): For e₁ e₂:
- infer Γ ⊢ e₁ : τ₁, Γ ⊢ e₂ : τ₂,
- assert τ₁ must be τ₂ -> β for fresh β,
- unify τ₁ with τ₂ -> β, giving substitution S,
- result type is S β.
Let: For let x = e₁ in e₂:
- infer Γ ⊢ e₁ : τ₁,
- generalize τ₁ to σ = Gen(Γ, τ₁),
- infer Γ, x:σ ⊢ e₂ : τ₂,
- result type is τ₂.

Algorithm W

See Algorithm W