Re: GADTs in the wild

Christopher Done wrote:

On 18 August 2012 20:57, Bertram Felgenhauer 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