GADT question

Thomas Jäger thjaeger at
Mon Oct 10 18:30:25 EDT 2005

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

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.



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

More information about the Glasgow-haskell-users mailing list