# Unification

What does it mean to solve a set of constraints? To answer this
question, we define *type substitutions*. A type substitution is a map
from a type variable to a type. We'll write `{t/X}`

for the
substitution that maps type variable `X`

to type `t`

. The way a
substitution `S`

operates on a type can be defined recursively:

```
S(X) = if S = {t/X} then t else X
S(t1 -> t2) = S(t1) -> S(t2)
```

A substitution `S`

can be applied to a constraint `t = t'`

; the result
`S(t = t')`

is defined to be `S(t) = S(t')`

. And a substitution can be
applied to a set `C`

of constraints; the result `S(C)`

is the result of
applying `S`

to each of the individual constraints in `C`

.

Given two substitutions `S`

and `S'`

, we write `S;S'`

for their
composition: `(S;S')(t) = S'(S(t))`

.

A substitution *unifies* a constraint `t_1 = t_2`

if `S(t_1) = S(t_2)`

.
A substitution `S`

unifies a set `C`

of constraints if `S`

unifies every
constraint in `C`

. For example, substitution
`S = {int->int/Y};{int/X}`

unifies constraint `X -> (X -> int) = int -> Y`

.

To solve a set of constraints `C`

, we need to find a substitution that
unifies `C`

. If there are no substitutions that unify `C`

, where `C`

is the constraints generated from expression `e`

, then `e`

is not
typeable.

To find a substitution that unifies `C`

, we use an algorithm
appropriately called the *unification* algorithm. It is defined as
follows:

if

`C`

is the empty set, then`unify(C)`

is the empty substitution.if

`C`

is the union of a constraint`t = t'`

with other constraints`C'`

, then`unify(C)`

is defined as follows, based on that constraint:if

`t`

and`t'`

are both the same type variable, e.g.`X`

, then return`unify(C')`

.if

`t = X`

for some type variable`X`

, and`X`

does not occur in`t'`

, then let`S = {t'/X}`

, and return`unify(S(C'));S`

.if

`t' = X`

for some type variable`X`

, and`X`

does not occur in`t`

, then let`S = {t/X}`

, and return`unify(S(C'));S`

.if

`t = t0 -> t1`

and`t' = t'0 -> t'1`

, then let`C''`

be the union of`C'`

with the constraints`t0 = t'0`

and`t1 = t'1`

, and return`unify(C'')`

.if

`t = t0 * t1`

and`t' = t'0 * t'1`

, then let`C''`

be the union of`C'`

with the constraints`t0 = t'0`

and`t1 = t'1`

, and return`unify(C'')`

.if

`t = (t0, ..., tn) tc`

and`t' = (t'0, ..., t'n) tc`

for some type constructor`tc`

, then let`C''`

be the union of`C'`

with the constraints`ti = t'i`

, and return`unify(C'')`

.otherwise, fail. There is no possible unifier.

In the second and third subcases, the check that `X`

should
not occur in `t`

ensures that the algorithm doesn't produce a cyclic
substitution—for example, `{(X -> X) / X}`

.

It's possible to prove that the unification algorithm always terminates,
and that it produces a result if and only a unifier actually exists—that
is, if and only if the set of constraints has a solution. Moreover, the
solution the algorithm produces is the *most general unifier*, in the
sense that if `S = unify(C)`

and `S'`

unifies `C`

, then there
must exist some `S''`

such that `S' = S;S''`

.

If `R`

is the type variable assigned to represent the type of the entire
expression `e`

, and if `S`

is the substitution produced by the
algorithm, then `S(R)`

is the type inferred for `e`

by HM type
inference. Call that type `t`

. It's possible to prove `t`

is the
*principal* type for the expression, meaning that if `e`

also has type
`t'`

for any other `t'`

, then there exists a substitution `S`

such that
`t' = S(t)`

. So HM actually infers the most lenient type that is possible
for any expression.

## Let expressions

Consider the following code:

```
let double f z = f (f z) in
(double (fun x -> x+1) 1, double (fun x -> not x) false)
```

The inferred type for `f`

in `double`

would be `X -> X`

. In the
algorithm we've described so far, the use of `double`

in the first
component of the pair would produce the constraint `X = int`

, and the
use of `double`

in the definition of `b`

would produce the constraint ```
X
= bool
```

. Those constraints would be contradictory, causing unification
to fail!

There is a very nice solution to this called *let-polymorphism*, which
is what OCaml actually uses. Let-polymorphism enables a polymorphic
function bound by a `let`

expression behave as though it has multiple
types. The essential idea is to allow each usage of a polymorphic
function to have its own instantiation of the type variables, so that
contradictions like the one above can't happen. We won't cover
let-polymorphism here.