[Haskell-cafe] GADT question
John Meacham
john at repetae.net
Mon Dec 5 20:37:18 EST 2005
I have been trying to learn GADTs but feel I don't quite grok them yet.
I am playing with an implementation of SPJ's algorithm from
http://research.microsoft.com/Users/simonpj/papers/higher-rank/index.htm
in it, he has a data type that represents a type, but with several
special cases that can't easily be expressed in haskell proper. I was
thinking GADTs might help but havn't been able to come up with something
good and was hoping someone could point me in the right direction or let
me know what I am trying to do is impossible/improbable.
right now, it looks like so
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. 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
but this is obviously not right, it can't create Rho types at all,
Fun should change a Sigma into a Rho but leave Tau the same, Fun should
be able to be applied to different types infering the correct one. and a
function that accepts a Rho should be able to accept a Tau... (though
explicit upconversions would be okay, meaning I need to create TyCons
for example with type 'Type Rho' in the upconverter)
anyone have any ideas on how to make this work? is this even possible to
express with GADTs?
John
--
John Meacham - ⑆repetae.net⑆john⑈
More information about the Haskell-Cafe
mailing list