GADTs in the wild

[Bertram Felgenhauer]

Christopher Done wrote:
> The context
> ===========
> 
> In a fat-client web app (like GMail) you have the need to send requests
> back to the server to notify the server or get information back, this is
> normally transported in JSON format. For a Haskell setup, it would be:
> 
>     JavaScript (Client) → JSON → Haskell (Server)
> 
> I made Fay, a Haskell subset that compiles to JavaScript to displace
> JavaScript in this diagram and now it's:
> 
>     Haskell (Client) → JSON → Haskell (Server)
[snip]
> I declare my GADT of commands, forcing the input type and the return
> type in the parameters. The Foreign instance is just for Fay to allow
> things to be passed to foreign functions.
> 
>     -- | The command list.
>     data Command where
>       GetFoo :: Double -> Returns Foo -> Command
>       PutFoo :: String -> Returns Double -> Command
>       deriving Read
>     instance Foreign Command

The natural encoding as a GADT would be as follows:

    data Command result where
        GetFoo :: Double -> Command Foo
        PutFoo :: String -> Command Double

For the client/server communication channel, the GADT poses a challenge:
serialisation and deserialisation. The easiest way to overcome that
problem is to use an existential.

    data SerializableCommand = forall a. Cmd (Command a)

Ideally, dispatch becomes

    dispatch :: Command a -> Snap a
    dispatch cmd =
      case cmd of
        GetFoo i -> return (Foo i "Sup?" True)
        ...

But you also have to transfer the result, and there is nothing you can
do with the result returned by 'dispatch'. This can be solved by adding
a suitable constraint to the Command type, say,

    data SerializableCommand = forall a. Foreign a => Cmd (Command a)

The client code would use

    call :: Foreign a => Command a -> (a -> Fay ()) -> Fay ()
    call cmd g = ajaxCommand (Cmd cmd) g

and the server would basically run a loop

    server :: (Command a -> Snap a) -> Snap ()
    server dispatch = loop where
        dispatch' (Cmd command) = do
            result <- dispatch command
            writeLBS $ encode . showToFay $ result
        loop = do
            cmd <- nextCommand
            dispatch' cmd
            loop

(All code is pseudo code, I have not even compiled it.)

Maybe this helps.

Best regards,

Bertram

P.S. The same idea of encoding commands in a GADT forms the basis of
'operational' and 'MonadPrompt' packages on Haskell, which allow to
define abstract monads (by declaring a 'Command' (aka 'Prompt') GADT
specifying the monad's builtin operations) and run them with as many
interpreters as one likes. The earliest work I'm aware of is
Chuan-kai Lin's "Programming monads operationally with Unimo" paper
at ICFP'06.

This usage of a 'Command' GADT can be viewed as a very shallow
application of the expression evaluator pattern, but it has quite a
different flavor in practice.