GADTs in the wild

[Christopher Done]

Oh, I went for a walk and realised that while I started with a GADT, I
ended up with a normal Haskell data type in a fancy GADT dress. I'll
get back to you if I get the GADT approach to work.

On 17 August 2012 15:14, Christopher Done <chrisdone at gmail.com> wrote:
> Funny, I just solved a problem with GADTs that I couldn't really see how
> to do another way.
>
>
> 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)
>
>
> Three problems to solve
> =======================
>
> There are three problems that I wanted to solve:
>
> 1. Make serialization "just work", no writing custom JSON instances or
> whatnot. That problem is solved. So I can just write:
>
>     get "some-request" $ \(Foo bar mu) -> …
>
> 2. Share data type definitions between the client and server code. That
> problem is solved, at least I have a solution that I like. It's like
> this:
>
>     module SharedTypes where
>     … definitions here …
>
>     module Client where
>     import SharedTypes
>
>     module Server where
>     import SharedTypes
>
> Thus, after any changes to the data types, GHC will force the programmer
> to update the server AND the client. This ensures both systems are in
> sync with one-another. A big problem when you're working on large
> applications, and a nightmare when using JavaScript.
>
> 3. Make all requests to the server type-safe, meaning that a given
> request type can only have one response type, and every command which is
> possible to send the server from the client MUST have a response. I have
> a solution with GADTs that I thing is simple and works.
>
>
> The GADTs part
> ==============
>
> module SharedTypes where
>
> 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
>
> Where `Returns' is a simple phantom type. We'll see why this is
> necessary in a sec.
>
>     -- | A phantom type which ensures the connection between the command
>     -- and the return value.
>     data Returns a = Returns
>       deriving Read
>
> And let's just say Foo is some domain structure of interest:
>
>     -- | A foobles return value.
>     data Foo = Foo { field1 :: Double, field2 :: String, field3 :: Bool }
>       deriving Show
>     instance Foreign Foo
>
> Now in the Server module, I write a request dispatcher:
>
>     -- | Dispatch on the commands.
>     dispatch :: Command -> Snap ()
>     dispatch cmd =
>       case cmd of
>         GetFoo i r -> reply r (Foo i "Sup?" True)
>
> Here is the "clever" bit. I need to make sure that the response Foo
> corresponds to the GetFoo command. So I make sure that any call to
> `reply` must give a Returns value. That value will come from the nearest
> place; the command being dispatched on. So this, through GHC's pattern
> match exhaustion checks, ensures that all commands are handled.
>
>     -- | Reply with a command.
>     reply :: (Foreign a,Show a) => Returns a -> a -> Snap ()
>     reply _ = writeLBS . encode . showToFay
>
> And now in the Client module, I wanted to make sure that GetFoo can only
> be called with Foo, so I structure the `call` function to require a
> Returns value as the last slot in the constructor:
>
>     -- | Call a command.
>     call :: Foreign a => (Returns a -> Command) -> (a -> Fay ()) -> Fay ()
>     call f g = ajaxCommand (f Returns) g
>
> The AJAX command is a regular FFI, no type magic here:
>
>     -- | Run the AJAX command.
>     ajaxCommand :: Foreign a => Command -> (a -> Fay ()) -> Fay ()
>     ajaxCommand =
>       ffi "jQuery.ajax({url: '/json', data: %1,\
>           "dataType: 'json', success : %2 })"
>
> And now I can make the call:
>
>     -- | Main entry point.
>     main :: Fay ()
>     main = call (GetFoo 123) $ \(Foo _ _ _) -> return ()
>
>
> Summary
> =======
>
> So in summary I achieved these things:
>
> * Automated (no boilerplate writing) generation of serialization for
>   the types.
> * Client and server share the same types.
> * The commands are always in synch.
> * Commands that the client can use are always available on the server
>   (unless the developer ignored an incomplete-pattern match warning, in
>   which case the compiler did all it could and the developer deserves
>   it).
>
> I think this approach is OK. I'm not entirely happy about "reply r". I'd
> like that to be automatic somehow.
>
>
> Other approaches / future work
> ==============================
>
> I did try with:
>
>     data Command a where
>       GetFoo :: Double -> Command Foo
>       PutFoo :: String -> Command Double
>
> But that became difficult to make an automatic decode instance. I read
> some suggestions by Edward Kmett:
> http://www.haskell.org/pipermail/haskell-cafe/2010-June/079402.html
>
> But it looked rather hairy to do in an automatic way. If anyone has any
> improvements/ideas to achieve this, please let me know.