GADTs in the wild

[Bertram Felgenhauer]

Christopher Done wrote:
> On 18 August 2012 20:57, Bertram Felgenhauer
> <bertram.felgenhauer at googlemail.com> wrote:
> > The natural encoding as a GADT would be as follows:
> >
> >     data Command result where
> >         GetFoo :: Double -> Command Foo
> >         PutFoo :: String -> Command Double
> >
> 
> Right, that's exactly what I wrote at the end of my email.

Sorry, I missed that.

> And then
> indeed dispatch would be `dispatch :: Command a -> Snap a`. But how do
> you derive an instance of Typeable and Read for this data type? The
> Foo and the Double conflict and give a type error.

Right. A useful Read instance can't be implemented at all for the
GADT. I'm unsure about Typeable. You have to provide the instances
for the existential wrapper (SerializableCommand) instead, which defeats
automatic deriving. And this wrapper almost isomorphic to the non-GADT
Command type that you ended up using.

So the trade-off is between some loss of type safety and having to
write boilerplate code.

The obvious question then is how to automate the boilerplate code
generation. In principle, Template Haskell is equipped to deal with
GADTs, but I see little existing work in this direction. There is
derive-gadt on hackage, but at a glance the code is a mess and the main
idea seems to be to provide separate instances for each possible
combination of type constructor and type argument. (So there would be
two Read instances for the type above, Read (Command Foo) and
Read (Command Double)), which is going in the wrong direction.
I suspect that the code will not be useful. Is there anything else?

Best regards,

Bertram