[Haskell-cafe] Re: generalised algebraic data types,
existential types, and phantom types
Jim Apple
japple at freeshell.org
Thu Jul 22 12:06:39 EDT 2004
I tried to post this to gmane.comp.lang.haskell.general, but it never
got there - it may belong here anyway.
Abraham Egnor wrote:
> Is there any closer approximation [of GADTs] possible?
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
data Term a = forall b . (EqType a b, EqType b Int) => Lit Int
| forall b . (EqType a b, EqType b Int) => Inc (Term Int)
| forall b . (EqType a b, EqType b Bool) => IsZ (Term Int)
| If (Term Bool) (Term a) (Term a)
| forall b . Fst (Term (a,b))
| forall b . Snd (Term (b,a))
| forall b c . (EqType a (b,c))=> Pair (Term b) (Term c)
class EqType a b | a->b, b->a
instance EqType a a
Unfortunately, I can't seem to write an eval function:
eval (Lit a) = a
gives
Inferred type is less polymorphic than expected
Quantified type variable `b' is unified with `Int'
When checking an existential match that binds
The pattern(s) have type(s): Term Int
The body has type: Int
In the definition of `eval': eval (Lit x) = x
Any ideas?
Jim
More information about the Haskell-Cafe
mailing list