# [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

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  and . Pasalic  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

Typing Dynamic Typing, Arthur Baars and Doaitse Swierstra. ICFP 2002.
http://www.cs.uu.nl/~arthurb/dynamic.html

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

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
>
> _______________________________________________