GADT question

[Thomas Jäger]

Hi Garret,

As others have mentioned, this is currently not supported, but it seems
that it will be at some point. On the sf bug-tracker, I could find the
following entries, but the issue has also been discussed on the mailing
list.
http://sourceforge.net/tracker/index.php?func=detail&aid=1116210&group_id=8032&atid=108032
http://sourceforge.net/tracker/index.php?func=detail&aid=1180651&group_id=8032&atid=108032

Interestingly, unlike in the constrained-datatype-case, ghc's run-time
representation of constrained gadts contains the dictionary, but there
is no way to access it (well, except unsafeCoerce#) that I am aware of.

So, how can we fake the desired behavior? Existential quantification
allows us to store and access a dictionary, and we can witness type
equality using GADTs, as in the E datatype below. Notice that

  Fractional b => f b

can be expressed as
  
  exists a. (Fractional a) and (a = b) => f b

Therefore, the following dataype is equivalent to yours and eval can be
implemented on top of it.

data E :: * -> * -> * where E :: E a a

data Term :: * -> * where
  Lit :: a -> Term a
  Div :: Fractional a => E a b -> Term a -> Term a -> Term b
  
eval :: Term a -> a
eval (Lit i) = i
eval (Div e t u) = let q = eval t / eval u in case e of E -> q

The case for Div is a little awkward, as ghc needs to be forced to unify
type variables and resolve constraints in a specific order for the trick
to work.


Regards,

Thomas


On Mon, 2005-10-10 at 13:06 -0400, J. Garrett Morris wrote:
> I've been attempting to use GADTs to create a small domain specific
> language, and I'm running into an odd problem.  Adding one case to the
> example at the beginning of the Wobbly types paper:
> 
> data Term :: * -> *
>     where Lit :: a -> Term a
>           Div :: Fractional a => Term a -> Term a -> Term a

> and extending the eval function accordingly:
> 
> eval :: Term a -> a
> eval (Lit i) = i
> eval (Div t u) = eval t / eval u