7
$\begingroup$

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)
$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.