[Haskell-cafe] Re: generalised algebraic data types,
existential types, and phantom types
Arthur Baars
arthurb at cs.uu.nl
Fri Jul 23 05:33:18 EDT 2004
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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
More information about the Haskell-Cafe
mailing list