# Introduction to Unification

7 January, 2017

Unification is a vital process in the implementation of Hindley-Damas-Milner type inference. In the original paper it is mentioned in passing as assumed knowledge, so here is an explanation of unification in with a little help from the HM type theory.

## What is Unification?

Unification is a method of solving equations by substitution. This sentence alone doesn’t give enough information to implement an algorithm, so let’s define some vocabulary to write a more rigorous definition.

`term`

: A term is an abstract syntax tree representing the language that will be used.
In order for unification to proceed, term must have some value that represents a
`variable`

, and some values that represent `constants`

- the idea being that `variables`

can be replaced during unification, but constants cannot.

`equation`

: An equation is a pair of terms, written `term_1 = term_2`

.

`syntactic equality`

: Two terms are syntactically equal if their ASTs match
exactly.

`equivalence`

: Two terms are equivalent if there exists some substitution that would
make them syntactically equal.

`solved`

: An equation is solved if the left and right hand sides are syntactically
equal.

`substitution`

: A substitution is a set of mappings from variables to terms, written
`{ var_1 => term_1, ..., var_i => term_i }`

.

`application`

: A substitution can be `applied`

to a value containing variables - written `subs(value)`

:

- term: by replacing variables with terms per each mapping
- equation: by applying the substitution to both sides
- set of equations: by applying the substitution to each element in the set
- substitution: by applying the substitution to the right hand side of each mapping

Applying an empty substitution to a value does not change the value.
For reasons that will be explained later, a substitution is only valid if every
variable on the left side of mapping does *not* occur in the term on the right
side of the respective mapping.

`minimal`

: A substitution is minimal if no variables in the right hand sides of
any mapping occur on any left hand side of any mapping. In other words, if
applying the substitution is idempotent: `subs(subs(value)) = subs(value)`

With this vocabulary, we can now better define unification:

*Given a set of equations eqs, find a minimal substitution sub such that
every equation in sub(eqs) is solved*

## Hindley-Milner

Unification is the backbone of type inference in the HM type theory. The actual type inference algorithm is not important here- just how unification works on HM terms.

A term in HM is defined as `term := term -> term | primitive | variable`

where
`primitive`

is an element of a set of primitive types and `variable`

is a string.
respectively. To satisfy the requirements of unification, primitives are constants
and variables are, of course, variables.

Examples of syntactically equal HM terms:

`a`

and`a`

`primitive`

and`primitive`

`a -> a`

and`a -> a`

Examples of equivalent HM terms:

`a`

and`c`

`primitive`

and`d`

`(a -> b) -> c`

and`d -> e`

When conducting type inference for an expression, its type is initially set to a new variable. A set of equations is generated by traversing the expression’s AST, then these equations are then unified, which yields a solution for the expression’s type variable.

## An Algorithm

A simple unification algorithm can be described as follows:

```
unify(equations):
solutions := {}
ix := 0
while ix < equations.length:
equation := equations[ix]
if solved(equation):
ix++
continue
substitution := {}
if is_variable(equation.lhs):
if occurs(equation.lhs, equation.rhs):
error("Variable occurred on both sides of an equation")
substitution := {current.lhs => current.rhs}
ix++
elif is_variable(equation.rhs):
swap_sides(equations[ix])
elif equivalent(equation.lhs, equation.rhs):
substitution := unify(implied_equations(equation))
else:
error("Cannot unify non-equivalent terms")
substitution.apply(solutions)
substitution.apply(equations)
solutions.union(substitution)
return solutions
```

In essence the algorithm is “rearrange an equation so it is a solution, update everything according to this knowledge, remember the solution and continue”. Sounds like something we did a lot in school…

### Why check `occurs`

?

This algorithm requires a substitution to ‘eliminate’ a variable from the problem. If a variable could also be on the right side of a substitution then it would not be eliminated, constructing an infinite solution.

To demonstrate, let’s unify the HM equations `{a = b -> c, a = d, b = d, a = c}`

without
the occurs check:

```
equations = {a = b -> c, a = d, b = d, a = c}
solutions = {}
equations = {b -> c = d, b = d, b -> c = c} (removed a = b -> c, applied a => b -> c)
solutions = {a => b -> c} (added a => b -> c)
equations = {b = b -> c, b -> c = c} (removed b -> c = d, applied d = b -> c)
solutions = {a => b -> c, d => b -> c} (added d => b -> c)
equations = {(b -> c) -> c = c} (removed b = b -> c, applied b = b -> c)
solutions = {a => (b -> c) -> c, d => (b -> c) -> c, b => b -> c} (applied then added b => b -> c)
equations = {}
solutions = {a => (b -> (b -> c) -> c) -> c, d => (b -> (b -> c) -> c) -> (b -> c) -> c, b => b -> (b -> c) -> c, c = (b -> c) -> c} (applied then added c => (b -> c) -> c)
apply solutions to original equations - remember that the solutions should solve all the original equations:
a = b -> c
b -> (b -> c) -> c = b -> c (using a => ...)
b -> (b -> (b -> c) -> c) -> (b -> c) -> c = b -> (b -> c) -> c (using c => ...)
no matter how many times we do this the equation will never be solved...
```

Omitting the occurs check does *not* unify the equations according our definition.

## Resources

The Wikipedia entry for Unification is amazing and goes into much more depth.