Re: generalised algebraic data types, existential types, and phantom types
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
You could make use of the equality data type[1,2]: newtype Equal a b = Eq (forall f . f a -> f b) cast :: Equal a b -> (a -> b) cast (Equal f) = f id Your data type would be: data Term a = Lit Int (Equal Int a) | Inc (Term Int) (Equal Int a) | ... | forall b c . Pair (Term b) (Term c) (Equal (b,c) a) eval :: Term a -> a eval (Lit x eq) = cast x eq eval ... = ... A value of type 'Equal a b' serves as a proof that 'a' and 'b' are equal. Its use is described in [1] and [2]. Pasalic [3] makes use of this type to implement typed abstract syntax. This paper describes what you are trying to achieve with your 'Term' data type. Arthur [1]Typing Dynamic Typing, Arthur Baars and Doaitse Swierstra. ICFP 2002. http://www.cs.uu.nl/~arthurb/dynamic.html [2]A lightweight implementation of generics and dynamics, James Cheney and Ralf Hinze. Haskell Workshop 2002, Pittsburgh, PA, 2002. http://www.cs.cornell.edu/people/jcheney/papers/Dynamic-final.pdf [3]Emir Pasalic: Meta-Programming with Typed Object-Language Representations. http://www.cse.ogi.edu/~pasalic/ On 22-jul-04, at 18:06, Jim Apple wrote:
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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (2)
-
Arthur Baars -
Jim Apple