[Haskellcafe] GADT question
Simon PeytonJones
simonpj at microsoft.com
Tue Dec 6 05:33:20 EST 2005
 I would like the type system to distinguish the three types and
enforce
 their properties. so far, I have come up with the following:


 data Sigma
 data Tau
 data Rho

 data Type a where
 ForAll :: [Id] > Type Rho > Type Sigma
 Fun :: Type a > Type a > Type a
 TyCon :: TyCon > Type Tau
 TyVar :: TyVar > Type Tau
It looks as if you want a kind of subtyping relationship, so that Tau <
Rho < Sigma. The standard way to achieve that is using polymorphism
(see, for example, papers about FFI to objectoriented languages)
data Sigma a = S a
data Rho a = R a
data Tau = Tau
data Type a where
 ForAll :: [Id] > Type (Sigma (Rho a)) > Type (Sigma b)
 Fun :: Type a > Type a > Type a
 TyCon :: TyCon > Type (Sigma (Rho Tau))
 TyVar :: TyVar > Type (Sigma (Rho Tau))
I'm not sure if this would work.
Simon
More information about the HaskellCafe
mailing list