Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier

Question

I'm trying to get a deep understanding of a (great) paper "Typing Haskell in Haskell". I'm having difficulties understanding the implementation of two methods there — the mgu and match.

Let's talk about the TAp case (full implementation in the article):

-- Substitutions are from a type variable to a type
type Subst  = [(Tyvar, Type)]


-- Calculate most general unifier 's' so that:
-- prop> apply s t1 = apply s t2
mgu :: Monad m => Ty.Type -> Ty.Type -> m Subst
mgu (TAp l r) (TAp l' r') = do s1 <- mgu l l'
                               s2 <- mgu (apply s1 r) (apply s1 r')
                               return (s2 @@ s1)              -- <=== THIS
-- ...snip...


-- Matching of t1 and t2 finds a substitution 's' so that:
-- prop> apply s t1 = t2
match :: Monad m => Type -> Type -> m Subst
match (TAp l r) (TAp l' r') = do sl <- match l l'
                                 sr <- match r r'
                                 merge sl sr                  -- <=== THIS
-- ...snip...


-- Substitution composition such that:
-- prop> apply (s1 @@ s2) = apply s1 . apply s2
(@@)       :: Subst -> Subst -> Subst
s1 @@ s2    = [ (u, apply s1 t) | (u,t) <- s2 ] ++ s1


-- A `symmetric' composition of substitutions such that:
-- prop> apply (s1++s2) = apply (s2++s1)
merge :: Monad m => Subst -> Subst -> m Subst
merge s1 s2 = if agree then return (s1 ++ s2) else fail "merge fails"
  where agree = all (\v -> apply s1 (Ty.TVar v) == apply s2 (Ty.TVar v))
                    (map fst s1 `intersect` map fst s2)

match is used only for matching predicates, mgu is used more often e.g. for actual type inference.

I can't wrap my head on why in the mgu the substitution composition is sequential and in match a symmetric composition is used. Why's that?

Furthermore, would it make a difference if I'd change the ordering of unification, so mgu would read:

mgu (TAp l r) (TAp l' r') = do s1 <- mgu r r'
                               s2 <- mgu (apply s1 l) (apply s1 l')
                               return (s2 @@ s1)

Answer 1

Ok, so I figured it out the next day. It's all dead simple as it came out.

Let's use an example – type applications z a a and z a b where z :: * -> * -> *. The unification will yield that (without further context) z a a is the most general type for both giving substitution {b↦a}. On the other hand, z a a cannot be matched to z a b, as they are simply different.

So now let's dissect the implementations. The mgu x@(TAp l r) y@(TAp l' r') first compares l and l' giving a substitution s1 <- mgu l l'. The s1 is a knowledge of how part of x and y are different. With that knowledge, we can investigate further; that's why we use apply in s2 <- mgu (apply s1 l) (apply s1 l') which gives us next premises on how different x and y are. So the summary is to compose the knowledge: s2 @@ s1 (ordering is as in function composition, e.g. g (f (x)) can be written as (g ∘ f) (x)).

I believe (without a proof though) that it's possible to just use s2 <- mgu r r' and then try to combine s1 with s2 though some kind of recursion would be required. Also, I believe it's possible to match r with r' first and then match l with l'; the ordering is just to make error messages more obvious (order of reading in a file).

The match x@(TAp l r) y@(TAp l' r') is different. We must not approve the first example: z a a vs z a b. In order to do that we need to:

1. note that a from x would need to become a from y
2. note that a from x would need to become b from y
3. tell that the above two premises are contradictory

That's the reason to yielding strange substitutions like {a↦a} which is semantically equivalent to {} but allows for taking #1 into account. The symmetric composition takes this additional information. It doesn't put apply in the second sub-matching (match (apply s1 r) (apply s1 r')) since applying a substitution would make us lose information about contradictory premises.