[Haskell-cafe] Re: generalised algebraic data types, existential types, and phantom types

[Arthur Baars]

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
>