I E

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):

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:

Examples of equivalent HM terms:

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.