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

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

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

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

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

<ol>
<li>note that <code>a</code> from <code>x</code> would need to become <code>a</code> from <code>y</code></li>
<li>note that <code>a</code> from <code>x</code> would need to become <code>b</code> from <code>y</code></li>
<li>tell that the above two premises are contradictory</li>
</ol>

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

CC BY-SA 3.0
2014-07-15T13:20:31.890Z
2014-07-15T13:20:31.890Z
kgadek
<p>I'm trying to get a deep understanding of a (great) paper <a href="http://web.cecs.pdx.edu/~mpj/thih/">"Typing Haskell in Haskell"</a>. I'm having difficulties understanding the implementation of two methods there — the <code>mgu</code> and <code>match</code>.</p>

<p>Let's talk about the <code>TAp</code> case (<a href="http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tth_sEc6">full implementation in the article</a>):</p>

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


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


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


-- Substitution composition such that:
-- prop&gt; apply (s1 @@ s2) = apply s1 . apply s2
(@@)       :: Subst -&gt; Subst -&gt; Subst
s1 @@ s2    = [ (u, apply s1 t) | (u,t) &lt;- s2 ] ++ s1


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

<p><code>match</code> is <a href="http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tth_sEc7.1">used only for matching predicates</a>, <code>mgu</code> is used more often e.g. for <a href="http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tth_sEc10">actual type inference</a>.</p>

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

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

<pre><code>mgu (TAp l r) (TAp l' r') = do s1 &lt;- mgu r r'
                               s2 &lt;- mgu (apply s1 l) (apply s1 l')
                               return (s2 @@ s1)
</code></pre>

<type-theory><type-systems><type-inference><haskell>
Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier
kgadek
# Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier

(Asked by: username_0 on 2014-07-14)

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)

**Tags:** type-theory, type-systems, type-inference, haskell


---

## 1 answers

### Answer by username_0 on 2014-07-15. Score: 3 | Accepted answer

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.


---

