Typing unification algorithm for parameterized types using GADTs?
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>
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?
participants (2)
-
Ahn, Ki Yung -
Dan Licata