[Haskell] Re: Typing unification algorithm for parameterized types using GADTs?

[oleg at okmij.org]

Ki Yung Ahn posed a problem of first-order syntactic unification
over GADTs.

There posted code seem to exhibit two problems: one deals with kind
equality, and the other with unification. Let's start with the latter.
You have chosen to represent substitutions as functions from terms to
terms. That's OK. However, the following lines seems weird:

> unify (t1 :-> t2) (t1' :-> t2')           = unify t1 t1' . unify t2 t2'

We wish to unify two composite (constructed terms) whose head is :->.
Unification of t1 t1' gives a substitution, and so does the
unification of t2 and t2'. Now we should prove that the results are
compatible, that is, if the domains of both substitutions overlap, the
common variables are associated with unifyable values. But the
composition is the wrong operation here: the composition is a total
operation. So, if we unify (X :-> X) (term1 :-> term2) where X is a
free variable and term1 is distinct from term2, we are successful?
Indeed, unify X term1 succeeds, so is unify X term2. The composition
is total. The result can't be right. The line has to be re-written as
follows

> unify (t1 :-> t2) (t1' :-> t2')           = 
>     let s = unify t1 t1' in s `compose` unify (s t2) (s t2')

where
> compose s1 s2 t = loop t
>  where
>   s = s1 . s2
>   loop t = let t1 = s t in if t1 == t then t else loop t1

The fixpoint assures the substitution is idempotent, as behooves to
the result of unify.

Now, the type of unify is also a bit wrong:
> unify :: (Show v,Ord v) => Ty v k -> Ty v k -> Ty v k -> Ty v k
It should be
> unify :: (Show v,Ord v) => Ty v k -> Ty v k -> Ty v k' -> Ty v k'

Finally, we come to the issue of kind equality. In
> data Ty v k where
>   TyA   :: Ty v (k1 :~> k2) -> Ty v k1 -> Ty v k2

k1 is an existentially quantified type variable. When we wish to
compare (TyA t1l t1r) with (TyA t2l t2r), we first have to prove that
the kind of t1r is the same as t2r. Both kinds are existentially
quantified, there is no reason they must always be equal. So, we have
to use intensional equality.

> data Star = Star deriving (Show,Eq)  -- the kind *
> data k1 :~> k2 = k1 :~> k2 deriving (Show,Eq)

Well, deriving Eq is not useful here: we can't actually compare Star
with (k1 :~> k2) because they have different types. So, we need an
intensional representation of kinds, with a useful comparison
function. We should also re-write 

>   TyC   :: v -> k -> Ty v k

to use that representation. The final code follows.

{-# OPTIONS -fglasgow-exts #-}

import List

infixr :~> -- kind arrow

-- term algebra of kinds
data Star
data k1 :~> k2

-- A representation of kinds
data K k where
  KStar :: K Star
  KArr  :: K k1 -> K k2 -> K (k1 :~> k2)

infixr :-> -- type arrow
data Ty v k where
  TyV   :: v -> Ty v Star  -- all type vars are of kind *.
  (:->) :: Ty v Star -> Ty v Star -> Ty v Star
  TyC   :: v -> K k -> Ty v k
  TyA   :: Ty v (k1 :~> k2) -> Ty v k1 -> Ty v k2



-- Kind equality
data EQ a b where
  Refl :: EQ a a

-- compare two kinds. Return either Nothing or the witness of their
-- equality
keq:: K k1 -> K k2 -> Maybe (EQ k1 k2)
keq KStar KStar = Just Refl
keq (KArr k1l k1r) (KArr k2l k2r) = keq' (keq k1l k2l) (keq k1r k2r)
keq _ _ = Nothing

keq' :: Maybe (EQ k1l k2l) -> Maybe (EQ k1r k2r) ->
	Maybe (EQ (k1l :~> k1r) (k2l :~> k2r))
keq' (Just Refl) (Just Refl) = Just Refl
keq' _ _ = Nothing

-- inverse of the above
keqa :: Maybe (EQ (k1l :~> k1r) (k2l :~> k2r)) -> Maybe (EQ k1r k2r)
keqa (Just Refl) = Just Refl
keqa _ = Nothing

-- compare two types for their kinds.
tykeq :: Ty v k1 -> Ty v k2 -> Maybe (EQ k1 k2)
tykeq (TyV _) (TyV _) = Just Refl
tykeq (_ :-> _) (_ :-> _) = Just Refl
tykeq (TyC _ k1) (TyC _ k2) = keq k1 k2
tykeq (TyA t1 _) (TyA t1' _) = keqa (tykeq t1 t1')

-- term equality
instance Eq v => Eq (Ty v k) where
    TyV v1 == TyV v2 = v1 == v2
    (t1l :-> t1r) == (t2l :-> t2r) = t1l == t2l && t1r == t2r
    TyC v1 _ == TyC v2 _ = v1 == v2
    (TyA t1l t1r) == (TyA t2l t2r) = 
	teq'' (tykeq t1r t2r) t1r t2r &&
	teq'' (tykeq t1l t2l) t1l t2l
    _ == _ = False
teq'' :: Eq v => Maybe (EQ k1 k2) -> Ty v k1 -> Ty v k2 -> Bool
teq'' (Just Refl) t1 t2 = t1 == t2
teq'' _ _ _ = False

list = TyC "List" (KArr KStar KStar)
nil_t = TyA list (TyV "a") -- the `List a' type
nil'_t = TyA list (TyV "b") -- the `List b' type
cons_t = TyV "b" :-> TyA list (TyV "b") :-> TyA list (TyV "b")

instance Show v => Show (Ty v k) where
  show (TyV v)     = show v
  show (t1 :-> t2) = "("++show t1++"->"++show t2++")"
  show (TyC v _)   = show v
  show (TyA t1 t2) = "("++show t1++" "++show t2++")"

occurs :: Eq v => v -> Ty v k -> Bool
occurs x (TyV y)     = x == y
occurs x (t1:->t2)   = occurs x t1 || occurs x t2
occurs _ (TyC _ _)   = False
occurs x (TyA t1 t2) = occurs x t1 || occurs x t2

-- A substitution on types can be written as follows:

type Subst v k = Ty v k -> Ty v k
substt :: Eq v => (v,Ty v Star) -> Subst v k
substt (x,t1) t@(TyV y) | x == y    = t1
                        | otherwise = t
substt p      (t1 :-> t2)           = substt p t1 :-> substt p t2
substt _      t@(TyC _ _)           = t
substt p      (TyA t1 t2)           = substt p t1`TyA`substt p t2

compose s1 s2 t = loop t
 where
  s = s1 . s2
  loop t = let t1 = s t in if t1 == t then t else loop t1


unify_gen :: (Show v,Ord v) => Maybe (EQ k1 k2) -> Ty v k1 -> Ty v k2 ->
	     Subst v k'
unify_gen (Just Refl) t1 t2 = unify t1 t2
unify_gen _ _ _ = error "incompat kinds"

unify :: (Show v,Ord v) => Ty v k -> Ty v k -> Subst v k'
unify t1@(TyV x)  t2@(TyV y) | x == y     = id
                             | x <= y     = substt (x,t2)
                             | otherwise  = substt (y,t1)
unify (TyV x)     t          | occurs x t = error(show x++" occurs in "
                                                ++show t)
                             | otherwise  = substt (x,t)
unify t1          t@(TyV _)               = unify t t1
unify (t1 :-> t2) (t1' :-> t2')           = 
    let s = unify t1 t1' in s `compose` unify (s t2) (s t2')
unify (TyC a _)   (TyC b _)  | a == b     = id
                             | otherwise  = error(show a++" is not "
                                              ++show b)
unify (TyA t1 t2) (TyA t1' t2')           = 
    let s = unify_gen (tykeq t2 t2') t2 t2' 
	tn1  = s t1
	tn1' = s t1'
    in s `compose` unify_gen (tykeq tn1 tn1') tn1 tn1'
unify t1          t2                      = error(show t1++" is not "
                                                ++show t2)


test1 = unify nil_t nil_t  $ nil_t
test2 = unify nil_t cons_t $ nil_t
test3 = let s = unify nil_t nil'_t in (s nil_t, s nil'_t)
test4 = let t1 = (TyV "a" :-> TyV "b") 
	    t2 = (TyV "b" :-> TyC "unit" KStar)
	    s = unify t1 t2
	in (s t1, s t2)
-- (("unit"->"unit"),("unit"->"unit"))
-- Indeed, both types are the same