Algorithm W

type-theory

Definition

Algorithm W

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

Given a type environment and an expression , it computes either failure or a pair

where is a type substitution and is a monotype such that

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 be the identity substitution.

Variable

If , instantiate the type scheme:

Abstraction

For , choose a fresh type variable :

Equivalently, the recursive call is made under the extended environment .

Application

For , choose a fresh type variable :

Here denotes a most general unifier. The equation expresses that must be a function accepting the type of .

Let

For :

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

because they would require an infinite type.