[Haskell] Typing unification algorithm for parameterized types
Ahn, Ki Yung
kyagrd at gmail.com
Wed Feb 6 19:47:21 EST 2008
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>
More information about the Haskell