7/27/21
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
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 than 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 -> Boo) ->(Bool ->Bool)->Bool -> Bool
Review sketch
With our set or list of constraints, we do not have to worry about the order in which we process them. There is the issue of the occurs check, which the Most General Unifier (mgu) algorithm looks after. We are solving the constraint equations for t0 (t-zero) which is the type of the initial formula. In the general case, it is possible for there to be constraints that fail the occur check, but which are not used to solve for t-zero— we won't worry about that possibility. Then, as an algorithm outline, what we are going to do is
-- mgu has type mgu :: Type -> Type ->(Subst,String)
solve::[Constraint] -> (Subst,String)
solve [] = (nullSubst,"")
solve ((CEquivalent t1 t2):cs) = let
(subs,errorStr) = (mgu t1 t2)
(subsCs,errorStrCs) = solve (map (apply subs) cs)
in
(composeSubst subs subsCs, if errorStr == ""
then errorStrCs
else errorStr ++ " " ++ errorStrCs)
In English, the mgu algorithm will take two type expressions, considered to be unifiable, and return an ordered pair of a substitution and an (error) message. The solve algorithm will take list of constraints and return an ordered pair of a substitution and an (error) message. mgu is applied to the first constraint. If it produces a successful substitution, that substitution is applied 'simultaneously' to all the other constraints. Then the solve algorithm is applied to the remaining, possibly modified, constraints to produce another substitution which is composed with the first. Then that process is repeated until the constraint set is exhausted. If there are no errors, the final composite substitution will contain a solution for t-zero, which is the type of the initial formula.