[Haskell-cafe] GADT question
oleg at pobox.com
oleg at pobox.com
Mon Dec 5 22:49:26 EST 2005
John Meacham wrote:
> data Type = ForAll [TyVar] Rho -- Forall type
> | Fun Type Type -- Function type
> | TyCon TyCon -- Type constants
> | TyVar TyVar -- Always bound by a ForAll
> with the three synonyms and their constraints being
> type Sigma = Type
> type Rho = Type -- No top-level ForAll
> type Tau = Type -- No ForAlls anywhere
> I would like the type system to distinguish the three types and enforce
> their properties.
Perhaps the enclosed code might be of help. Tests:
test1 = TyCon "Int"
*Forall> :t test1
test1 :: Type FANil
test2 = Forall ["a"] (Fun (TyVar "a") (TyVar "a"))
*Forall> :t test2
test2 :: Type FATop
-- Inferred type!
test3 = Fun test2 test1
*Forall> :t test3
test3 :: Type FASomewhere
test3' = Fun test1 test1
*Forall> :t test3'
test3' :: Type FANil
test4 = Forall ["b"] test3
*Forall> :t test4
test4 :: Type FATop
test4' = Forall ["b"] test2 -- Error!
No instance for (RhoC FATop)
arising from use of `Forall' at /tmp/m.hs:43:9-14
That is, in test4, the second argument of Forall is not of the type
rho! Typeclasses would work too. I'm lacking a good example to show
off this machinery...
{-# OPTIONS -fglasgow-exts #-}
module Forall where
data FANil
data FATop
data FASomewhere
type Id = String
type Tau = Type FANil
data Type a where
Forall :: (RhoC a) => [Id] -> Type a -> Type FATop
Fun :: (FAMerge a b c) => Type a -> Type b -> Type c
TyCon :: Id -> Type FANil
TyVar :: Id -> Type FANil
type Sigma a = Type a
--type (RhoC a) => Rho a = Type a -- I wish that worked...
class RhoC a
instance RhoC FANil
instance RhoC FASomewhere
class FAMerge a b c | a b -> c
instance FAMerge FANil FANil FANil
instance FAMerge FANil FASomewhere FASomewhere
instance FAMerge FANil FATop FASomewhere
instance FAMerge FATop a FASomewhere
instance FAMerge FASomewhere a FASomewhere
test1 = TyCon "Int"
test2 = Forall ["a"] (Fun (TyVar "a") (TyVar "a"))
test3 = Fun test2 test1
test3' = Fun test1 test1
-- I guess we need to hide the data constructors of Type and use
-- functions like rho, fun, tycon, etc. to construct the values of
-- Type
rho :: (RhoC a) => Type a -> Type a
rho = id
test4 = Forall ["b"] test3
-- The following is error!
--test4' = Forall ["b"] test2
More information about the Haskell-Cafe
mailing list