Hindley-Milner III — Solving the Constraints

11/1/19

Solving the constraints

In the general case, this can be quite difficult. But fortunately our case is one of the easier ones. First of all, we can work through the constraints in any order we wish and address any constraint just once. In particular, we can just work left to right through them one at a time. The result will give us a substitution, under which all the constraints come out true, if that can be done.

Most General Unifier (MGU)

We need the notion of a Most General Unifier. Let us give an example, say we have a constraint

 t1=t2

and we are trying to find a substitution that satisfies it or under which the constraint comes out to be true. There are infinitely many of them, here are a few [t1:Int, t2: Int], [t1:Bool, t2: Bool], [t1:Bool->Int, t2: Bool->Int], etc. Now, we do not want to pick a single one of these at this stage, because it might be too specific and we might want something different with a later constraint (e.g. we might want Ints not Bools). The way around this is to go as general as we can, and in this case the most general substitution is [ t1:t2].

Some unsatisfiable constraints

Sometimes a constraint cannot be satisfied, for example

Int=Bool

cannot.

Occurs check

Another type of constraint that cannot be satisfied is where the variable on the left occurs within some structure on the right, for example

 t1=t2→t1

the problem here is that if t1 is substituted for on the right it introduces a t1 which itself must be substituted for (which itself introduces a t1 which itself must be substituted for.... forever). Of course, examples of this can be more complex, e.g.

t1=t2→(t3→t1)→t4

but the point remains: the type variable on the left must not 'occur' on the right. The same is true 'the other way around'; if a single type variable being matched from the right occurs within an expression on the left, that fails the occurs check.

A MGU algorithm sketch for these constraints

This algorithm takes a single constraint as input and returns either the error message that the two cannot be unified or a substitution whose application unifies them.

The algorithm should be read from top to bottom and it uses pattern matching on the form of the types.

unify (Int = Int)             = "success" Substitution = []      {- this means no substitution required -}

unify (Bool = Bool)      = "success" Substitution = []      {- this means no substitution required -}

unify (t =<anything>)   = if t occurs in <anything> then "fail" else "success" Substitution = [t:anything]

unify (<anything>=t)    = if t occurs in <anything> then "fail" else "success" Substitution = [t:anything]

unify (t1→t2 = t3→ t4 ) = if unify (t1= t3) is "success" with Substitution(s) = s1 and
                                          if unify (t2= t4) is "success" with Substitution(s) = s2
                                          then "success" with Substitution(s) = s1 ++ s2
                                                  
  else "fail'

unify (<anythingElse> =<anythingElse>) = "fail"

Dealing with a list of constraints

Usually there will be more that one constraint. A list of constraints is approached as follows. Use MGU on the first constraint, apply the resulting substitution to the constraints and to the existing substitutions, and repeat through the list (of course, if there is a "fail", you would stop at that point).

Here is an example. The formula

λx:B->B.λy:B->B.λz:B.(y (x z))

has constraints:

[t9 = t10 -> t8, t7 = t8 -> t6, t10 = t5, t5 = Bool, t4 = t5 -> t6, t7 = t3, t3 = Bool -> Bool, t2 = t3 -> t5 -> t6, t9 = t1, t1 = Bool -> Bool, t0 = t1 -> t3 -> t5 -> t6] 

so, looking through our MGU algorithm, we need to add t9:t10->t8 to our substitutions. Then apply that through the constraints and previous substitutions, and discard any trivial constraints. The result is

Substitutions; [t9:t10->t8]

Constraints:  [ t7 = t8 -> t6, t10 = t5, t5 = Bool, t4 = t5 -> t6, t7 = t3, t3 = Bool -> Bool, t2 = t3 -> t5 -> t6, t10->t8 = t1, t1 = Bool -> Bool, t0 = t1 -> t3 -> t5 -> t6] 

Then

Substitutions; [t9: t10->t8, t7: t8 -> t6]

Constraints:  [ t10 = t5, t5 = Bool, t4 = t5 -> t6,  t8 -> t6 = t3, t3 = Bool -> Bool, t2 = t3 -> t5 -> t6, t10->t8 = t1, t1 = Bool -> Bool, t0 = t1 -> t3 -> t5 -> t6]

Then

Substitutions; [t9: t5->t8, t7: t8 -> t6, t10: t5]

Constraints:  [ t5 = Bool, t4 = t5 -> t6,  t8 -> t6 = t3, t3 = Bool -> Bool, t2 = t3 -> t5 -> t6, t5->t8 = t1, t1 = Bool -> Bool, t0 = t1 -> t3 -> t5 -> t6]

Then

Substitutions; [t9:Bool->t8, t7: t8 -> t6, t10: Bool, t5: Bool]

Constraints:  [ t4 = Bool -> t6,  t8 -> t6 = t3, t3 = Bool -> Bool, t2 = t3 -> Bool -> t6, Bool->t8 = t1, t1 = Bool -> Bool, t0 = t1 -> t3 ->Bool -> t6] 

Then

Substitutions; [t9:Bool->t8, t7: t8 -> t6, t10: Bool, t5: Bool, t4: Bool -> t6, t3: t8 -> t6]

Constraints:  [t8 -> t6 = Bool -> Bool, t2 =t8 -> t6-> Bool -> t6, Bool->t8 = t1, t1 = Bool -> Bool, t0 = t1 ->t8 -> t6->Bool -> t6] 

Then

Substitutions; [t9:Bool->Bool, t7: Bool -> t6, t10: Bool, t5: Bool, t4: Bool -> t6, t3:Bool-> t6, t8: Bool]

Constraints:  [Bool -> t6 = Bool -> Bool, t2 =Bool -> t6-> Bool -> t6, Bool->Bool = t1, t1 = Bool -> Bool, t0 = t1 ->Bool -> t6->Bool -> t6] 

Then

Substitutions; [t9:Bool->Bool, t7: Bool -> Bool, t10: Bool, t5: Bool, t4: Bool -> Bool, t3:Bool-> Bool, t8: Bool, t6: Bool]

Constraints:  [t2 =Bool -> Bool-> Bool -> Bool, Bool->Bool = t1, t1 = Bool -> Bool, t0 = t1 ->Bool ->Bool->Bool -> Bool] 

Then

Substitutions; [t9:Bool->Bool, t7: Bool -> Bool, t10: Bool, t5: Bool, t4: Bool -> Bool, t3:Bool-> Bool, t8: Bool, t6: Bool, t2 : Bool -> Bool-> Bool -> Bool]

Constraints:  [Bool->Bool = t1, t1 = Bool -> Bool, t0 = t1 ->Bool ->Bool->Bool -> Bool]

Then

Substitutions; [t9:Bool->Bool, t7: Bool -> Bool, t10: Bool, t5: Bool, t4: Bool -> Bool, t3:Bool-> Bool, t8: Bool, t6: Bool, t2 : Bool -> Bool-> Bool -> Bool, t1: Bool -> Bool]

Constraints:  [t0 = Bool -> Bool ->Bool ->Bool->Bool -> Bool] 

At this point, we're done. All the constraints are satisfied. We know what the types are for all the subformulas. Although all we are interested in is a type for t0, the original formula. We have that: t0 = Bool -> Bool ->Bool ->Bool->Bool -> Bool.

The STLC formula

λx:B->B.λy:B->B.λz:B.(y (x z))

has type

Bool -> Bool ->Bool ->Bool->Bool -> Bool