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

[Ahn, Ki Yung]

I was writing a type inference algorithm for let-polymorphic type system
with parametrized types. (That is, the type system as type constructors
such as `Maybe'.)  Things work out nicely except for one equation in the
unification function.  I will illustrate my problem with the definitions
and examples that you can actually run.  You will need -XGADTs and
-XTypeOperators to run this as a literate Haskell script in ghc 6.8.2.

FYI, my problematic unification function appears at the end.
This is not that long article (about 150 lines), anyway.

> import List

First, we define the kind as follows:

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

Next, we define the type as GADTs indexed with kinds,

> 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 -> Ty v k
>   TyA   :: Ty v (k1 :~> k2) -> Ty v k1 -> Ty v k2

Note that, we only allow type variables to be of kind * (abbr. for Star).
For example, we define the parametrized type List as follows:

> list = TyC "List" (Star :~> Star)

So, we can give `nil' (empty list) the type

TyA list (TyV "a") -- the `List a' type

and `cons' the type

TyV "a" :-> TyA list (TyV "a") :-> TyA list (TyV "a")

We also define an instance for Show class,
since deriving does not support GATDs.

> 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++")"

Then, we can write some functions.

An occurs check on types can be written as follows:

> 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:

> substt :: Eq v => (v,Ty v Star) -> Ty v k -> Ty 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

Recall that we only have type variables of kind *. So, we only need to
substitute a variable to a type of kind *.

Finally, we try writing a unification function as follows:

> unify :: (Show v,Ord v) => Ty v k -> Ty v k -> Ty v k -> Ty 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')           = unify t1 t1' . unify t2 t2'
> unify (TyC a _)   (TyC b _)  | a == b     = id
>                              | otherwise  = error(show a++" is not "
>                                               ++show b)
> unify (TyA t1 t2) (TyA t1' t2')           = unify t1 t1' . unify t2 t2'
> unify t1          t2                      = error(show t1++" is not "
>                                                 ++show t2)

I think I may be able to make it go through by changing the representation
of unification to a data structure such as list of substitution pairs.

But, just out of curiosity, what kind of an operator should I define to
combine the result of two unifications (unify t1 t1') (unify t2 t2') properly
in this setting?

-- 
Ahn, Ki Yung <kya at pdx.edu>