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

[Dan Licata]

Hi Ki Yung,

I think the problem starts even on the left of the TyA case.  Let's turn
on -XScopedTypeVariables and put in some type annotations:

unify :: (Show v,Ord v) => Ty v k -> Ty v k -> Ty v k -> Ty v k
unify (TyA (t1 :: Ty v (k2 :~> k)) (t2 :: Ty v k2))
      (TyA (t1' :: Ty v (k2' :~> k)) (t2' :: Ty v k2')) =  
    let x = unify t1 t1' 
        y = unify t2 t2'
    in undefined

You've stated your unification algorithm so that it works on two types
of the same kind.  However, each time you invert the application rule,
which existentially quantifies over the argument kind of the function,
you get a different argument kind (here, I've named them k2 and k2').
Thus, it's not even type correct to call unification on t1 and t1', or
on t2 and t2', since they may have different kinds.  So you get a type
error on either of the two inductive calls, even when their types are
not constrained by the return type of the function.  One thing to try is
to generalize your function so that it compares two types of potentially
different kinds.

However, even if you successfully got the inductive calls to go through,
it wouldn't make sense to compose them: unify t1 t1' would be a 

Ty v (k2 :~> k) -> Ty v (k2 :~> k)

wheraes unify t2 t2' would be

Ty v k2 -> Ty v k2

If you want to represent the substitution resulting from unification as
a function that performs the substitution, you will at least have to
show this function that works on types of any kind, not just the kind of
the two terms you're comparing.  One way to do this might be to return a
polymorphic function (forall k. Ty v k -> Ty v k).

You might find the following discussion of unification by Frank Pfenning helpful:
http://www.cs.cmu.edu/~fp/courses/lp/lectures/06-unif.pdf 

-Dan

On Feb06, Ahn, Ki Yung wrote:
> 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?
>