Unification

type-theory

Definition

Unification

Unification is the problem of finding a substitution that makes two formal expressions equal.

Formally, for expressions $s$ and $t$, a substitution $S$ is a unifier iff

$$S(s)=S(t).$$

In type inference, unification is used to solve type equations such as

$${\tau }_1={\tau }_2.$$