Unification

Type Analysis
Skill: [3.5]

Unification is the process of finding an assignement of variables and expressions to types, so that typing constraints are satisfied (see Type Inference to see where the constraints come from).

Type of constraints

There are only two types of constraints in unification: 1. Typing constraints (binding a variable or an expression to a type expression) 2. Equality constraints between type expressions.

The Martelli Montanari algorithm puts the constraints in a list, and processes them one by one. What happens depends of the type of equality constraint, but it's usually either adding more constraints or making replacement of type variables in all the constraints.

Types of equality constraints

There are four types of equality constraints.

$\alpha = \alpha$: This is trivial, just remove the constraints
$\alpha = \beta$: Replace $\beta$ with $alpha$ everywhere
$\texttt{TypeCons}(\tau_1, \tau_2, \dots) = \texttt{TypeCons}(\tau_1', \tau_2', \dots): Add new constraints to the list, for example $\tau_1 = \tau_1'$.
$\alpha = \texttt{TypeCons}(\tau_1, \tau_2, \dots)$: Replace $\alpha$ with the right hand side everywhere.