Algorithm W

type-theory

Definition

Algorithm W

Algorithm W is a type inference algorithm for the Hindley–Milner type system.

Given a type environment $\Gamma$ and an expression $e$, it computes either failure or a pair

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

where $S$ is a type substitution and $\tau$ is a monotype such that

$$S\Gamma ⊢e:\tau .$$

Principle

Algorithm W traverses the expression bottom-up. It introduces fresh type variables for unknown types, generates equality constraints from function application, and solves them by unification.

If inference succeeds, the inferred type is a principal type.

Rules

Let $\mathrm{id}$ be the identity substitution.

Variable

If $x:\sigma \in \Gamma$, instantiate the type scheme:

$$W(\Gamma ,x)=(\mathrm{id},\mathrm{inst}(\sigma )).$$

Abstraction

For $\lambda x.e$, choose a fresh type variable $\alpha$:

$$\begin{array}{rl}W(\Gamma [x\mapsto \alpha ],e)& =(S_1,{\tau }_1),\\ W(\Gamma ,\lambda x.e)& =(S_1,S_1\alpha \to {\tau }_1).\end{array}$$

Equivalently, the recursive call is made under the extended environment $\Gamma ,x:\alpha$.

Application

For $e_1{e}_2$, choose a fresh type variable $\alpha$:

$$\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}$$

Here $\mathrm{mgu}$ denotes a most general unifier. The equation $S_2{\tau }_1={\tau }_2\to \alpha$ expresses that $e_1$ must be a function accepting the type of $e_2$.

Let

For $\mathbf{let}x=e_1\mathbf{in}{e}_2$:

$$\begin{array}{rl}W(\Gamma ,e_1)& =(S_1,{\tau }_1),\\ \sigma & =\mathrm{gen}(S_1\Gamma ,{\tau }_1),\\ W(S_1\Gamma [x\mapsto \sigma ],e_2)& =(S_2,{\tau }_2),\\ W(\Gamma ,\mathbf{let}x=e_1\mathbf{in}{e}_2)& =(S_2\circ S_1,{\tau }_2).\end{array}$$

The let rule is the only place where HM generalises a type into a polymorphic type scheme.

Failure

Algorithm W fails when unification fails. In particular, the occurs check rejects equations such as

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

because they would require an infinite type.