Solving Constraints

What does it mean to solve a set of constraints? Since constraints are equations on types, it's much like solving a system of equations in algebra. We want to solve for the values of the variables appearing in those equations. By substituting those values for the variables, we should get equations that are identical on both sides. For example, in algebra we might have:

5x + 2y =  9
 x -  y = -1

Solving that system, we'd get that x = 1 and y = 2. If we substitute 1 for x and 2 for y, we get:

5(1) + 2(2) =  9
  1  -   2  = -1

which reduces to

 9 =  9
-1 = -1

In programming languages terminology (though perhaps not high-school algebra), we say that the substitutions {1 / x} and {2 / y} together unify that set of equations, because they make each equation "unite" such that its left side is identical to its right side.

Solving systems of equations on types is similar. Just as we found numbers to substitute for variables above, we now want to find types to substitute for type variables, and thereby unify the set of equations.

Type substitutions

Much like the substitutions we defined before for the substitution model of evaluation, we'll write {t / 'x} for the type substitution that maps type variable 'x to type t. For example, {t2/'x} t1 means type t1 with t2 substituted for 'x.

We can define substitution on types as follows:

int {t / 'x} = int
bool {t / 'x} = bool
'x {t / 'x} = t
'y {t / 'x} = 'y
(t1 -> t2) {t / 'x} =  (t1 {t / 'x} ) -> (t2 {t / 'x} )

Given two substitutions S1 and S2, we write S1; S2 to mean the substitution that is their sequential composition, which is defined as follows:

t (S1; S2) = (t S1) S2

The order matters. For example, 'x ({('y -> 'y) / 'x}; {bool / 'y}) is bool -> bool, not 'y -> 'y. We can build up bigger and bigger substitutions this way.

A substitution S can be applied to a constraint t = t'. The result (t = t') S is defined to be t S = t' S. So we just apply the substitution on both sides of the constraint.

Finally a substitution can be applied to a set C of constraints; the result C S is the result of applying S to each of the individual constraints in C.

Unification

A substitution unifies a constraint t_1 = t_2 if t_1 S results in the same type as t_2 S. For example, substitution S = {int -> int / 'y}; {int / 'x} unifies constraint 'x -> ('x -> int) = int -> 'y, because

('x -> ('x -> int)) S
=
int -> (int -> int)

and

(int -> 'y) S
=
int -> (int -> int)

A substitution S unifies a set C of constraints if S unifies every constraint in C.

The unification algorithm

At last we can precisely say what it means to solve a set of constraints: we must find a substitution that unifies the set. That is, we need to find a sequence of maps from type variables to types, such that the sequence causes each equation in the constraint set to "unite", meaning that its left-hand side and right-hand side become the same.

To find a substitution that unifies constraint set C, we use an algorithm unify, which is defined as follows:

• If C is the empty set, then unify(C) is the empty substitution.

• If C contains at least one constraint t1 = t2 and possibly some other constraints C', then unify(C) is defined as follows:

  • If t1 and t2 are both the same simple type—i.e. both the same type variable 'x, or both int or both bool— then return unify(C'). In this case, the constraint contained no useful information, so we're tossing it out and continuing.

  • If t1 is a type variable 'x and 'x does not occur in t2, then let S = {t2 / 'x}, and return S; unify(C' S). In this case, we are eliminating the variable 'x from the system of equations, much like Gaussian elimination in solving algebraic equations.

  • If t2 is a type variable 'x and 'x does not occur in t1, then let S = {t1 / 'x}, and return S'; unify(C' S). This is an elimination like the previous case.

  • If t1 = i1 -> o1 and t2 = i2 -> o2, where i1, i2, o1, and o2 are types, then unify(i1 = i2, o1 = o2, C'). In this case, we break one constraint down into two smaller constraints and add those constraints back in to be further unified.

  • Otherwise, fail. There is no possible unifier.

In the second and third subcases, the check that 'x should not occur in the type ensures that the algorithm is actually eliminating the variable. Otherwise, the algorithm could end up re-introducing the variable instead of eliminating it.

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' also unifies C, then there must exist some S'' such that S' = S; S''. Such an S' is less general than S because it contains the additional substitutions of S''.