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@pdx.edu>