Simon Peyton-Jones | 14 Aug 13:32 2012
Picon

GADTs in the wild

Friends


I’m giving a series of five lectures at the Laser Summer School (2-8 Sept), on “Adventures with types in Haskell”.  My plan is:

1.   Type classes

2.   Type families [examples including Repa type tags]

3.   GADTs

4.   Kind polymorphism

5.   System FC and deferred type errors

 

This message is to invite you to send me your favourite example of using a GADT to get the job done.  Ideally I’d like to use examples that are (a) realistic, drawn from practice (b) compelling and (c) easy to present without a lot of background.  Most academic papers only have rather limited examples, usually eval :: Term t -> t, but I know that GADTs are widely used in practice.

 

Any ideas from your experience, satisfying (a-c)?  If so, and you can spare the time, do send me a short write-up. Copy the list, so that we can all benefit.

 

Many thanks


Simon

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Michael Snoyman | 14 Aug 13:44 2012

Re: GADTs in the wild



On Tue, Aug 14, 2012 at 2:32 PM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

Friends


I’m giving a series of five lectures at the Laser Summer School (2-8 Sept), on “Adventures with types in Haskell”.  My plan is:

1.   Type classes

2.   Type families [examples including Repa type tags]

3.   GADTs

4.   Kind polymorphism

5.   System FC and deferred type errors

 

This message is to invite you to send me your favourite example of using a GADT to get the job done.  Ideally I’d like to use examples that are (a) realistic, drawn from practice (b) compelling and (c) easy to present without a lot of background.  Most academic papers only have rather limited examples, usually eval :: Term t -> t, but I know that GADTs are widely used in practice.

 

Any ideas from your experience, satisfying (a-c)?  If so, and you can spare the time, do send me a short write-up. Copy the list, so that we can all benefit.

 

Many thanks


Simon


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Hi Simon,

In the webcast I gave last week, I used a dumbed-down version of how we do safe queries in Persistent. The example is on slides 20-22 of [1]. Persistent works mostly the same way (and was inspired in this usage by groundhog[2]). If you want a more thorough explanation of how Persistent uses GADTs, let me know.

An example that came up at work (with Yitzchak Gale, he probably has more details) was essentially two different types of documents that shared a lot of the same kinds of elements (tables, lists, paragraphs, etc) but some elements only appeared in one of the document types. We needed to render to (for sake of argument) two different XML formats, and wanted to be certain we didn't put in elements from type 1 in type 2. The solution looked something like this (using data kinds and GADTs):

data DocType = Doc1 | Doc2

data Element (doctype :: DocType) where
    Paragraph :: Text -> Element doctype
    Table :: [Element doctype] -> Element doctype
    ...
    BulletList :: [[Element doctype]] -> Element Doc1

renderDoc1 :: Element Doc1 -> XML
renderDoc2 :: Element Doc2 -> XML

Michael

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Felipe Almeida Lessa | 14 Aug 14:48 2012
Picon

Re: GADTs in the wild

On Tue, Aug 14, 2012 at 8:44 AM, Michael Snoyman <michael <at> snoyman.com> wrote:
> An example that came up at work (with Yitzchak Gale, he probably has more
> details) was essentially two different types of documents that shared a lot
> of the same kinds of elements (tables, lists, paragraphs, etc) but some
> elements only appeared in one of the document types. We needed to render to
> (for sake of argument) two different XML formats, and wanted to be certain
> we didn't put in elements from type 1 in type 2. The solution looked
> something like this (using data kinds and GADTs):

This is the same thing that I did on the fb library.  There are two
kinds of Facebook access tokens: an app access token and an user
access token.  Some methods require either one or the other (e.g.
[5]), but there are also some methods that may use whatever kind of
access token you have (e.g. [3,4]).  So AccessToken [1,2] is defined
as the following GADT:

  data AccessToken kind where
      UserAccessToken :: UserId -> AccessTokenData -> UTCTime ->
AccessToken UserKind
      AppAccessToken  :: AccessTokenData -> AccessToken AppKind

  data UserKind
  data AppKind

(Yes, that could be a data kind!)  And for convenience we also export
some type synonyms:

  type UserAccessToken = AccessToken UserKind
  type AppAccessToken = AccessToken AppKind

So we get the convenience of one data type and the type safety of two,
which is especially nice considering that there are functions
returning access tokens as well [6,7].

Cheers, =)

[1] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#t:AccessToken
[2] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/src/Facebook-Types.html#AccessToken
[3] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:isValid
[4] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:fqlQuery
[5] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:createCheckin
[6] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:getAppAccessToken
[7] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:getUserAccessTokenStep2

--

-- 
Felipe.
Christian Maeder | 14 Aug 17:52 2012
Picon

Re: GADTs in the wild

Am 14.08.2012 14:48, schrieb Felipe Almeida Lessa:
>    data AccessToken kind where
>        UserAccessToken :: UserId -> AccessTokenData -> UTCTime ->
> AccessToken UserKind
>        AppAccessToken  :: AccessTokenData -> AccessToken AppKind
>
>    data UserKind
>    data AppKind
>
> (Yes, that could be a data kind!)  And for convenience we also export
> some type synonyms:
>
>    type UserAccessToken = AccessToken UserKind
>    type AppAccessToken = AccessToken AppKind

Why not use plain h98?

   data UserAccessToken = UserAccessToken UserId AccessTokenData UTCTime
   data AppAccessToken = AppAccessToken AccessTokenData

   type AccessToken = Either UserAccessToken AppAccessToken

C.
Felipe Almeida Lessa | 14 Aug 18:32 2012
Picon

Re: GADTs in the wild

2012/8/14 Christian Maeder <Christian.Maeder <at> dfki.de>:
> Why not use plain h98?
>
>   data UserAccessToken = UserAccessToken UserId AccessTokenData UTCTime
>   data AppAccessToken = AppAccessToken AccessTokenData
>
>   type AccessToken = Either UserAccessToken AppAccessToken

Convenience.  It's better to write

  case token of
    UserAccessToken ... -> ...
    AppAccessToken ... -> ...

than

  case token of
    Left (UserAccessToken ...) -> ...
    Right (UserAccessToken ...) -> ...

Also, it's easier to write

  isValid token

than

  isValid (Right token)  -- or is it Left?

Cheers, =)

--

-- 
Felipe.
Christian Maeder | 15 Aug 17:54 2012
Picon

Re: GADTs in the wild

Well, "Either" was an adhoc choice and should be application specific.
Another h98 solution would be to keep the common part in a single 
constructor:

   data UserOrAppData = AppData | UserData UserId UTCTime
   data AccessToken = AccessToken UserOrAppData AccessTokenData

or: data AccessToken a = AccessToken a AccessTokenData

C.

Am 14.08.2012 18:32, schrieb Felipe Almeida Lessa:
> 2012/8/14 Christian Maeder <Christian.Maeder <at> dfki.de>:
>> Why not use plain h98?
>>
>>    data UserAccessToken = UserAccessToken UserId AccessTokenData UTCTime
>>    data AppAccessToken = AppAccessToken AccessTokenData
>>
>>    type AccessToken = Either UserAccessToken AppAccessToken
>
> Convenience.  It's better to write
>
>    case token of
>      UserAccessToken ... -> ...
>      AppAccessToken ... -> ...
>
> than
>
>    case token of
>      Left (UserAccessToken ...) -> ...
>      Right (UserAccessToken ...) -> ...
>
> Also, it's easier to write
>
>    isValid token
>
> than
>
>    isValid (Right token)  -- or is it Left?
>
> Cheers, =)
>
Felipe Almeida Lessa | 15 Aug 17:58 2012
Picon

Re: GADTs in the wild

On Wed, Aug 15, 2012 at 12:54 PM, Christian Maeder
<Christian.Maeder <at> dfki.de> wrote:
> Well, "Either" was an adhoc choice and should be application specific.
> Another h98 solution would be to keep the common part in a single
> constructor:
>
>   data UserOrAppData = AppData | UserData UserId UTCTime
>   data AccessToken = AccessToken UserOrAppData AccessTokenData

This is a non-solution since you can't specify anymore that you want
an user access token but not an app access token.

> or: data AccessToken a = AccessToken a AccessTokenData

And this one brings us the Either again (although on fewer places).
Most functions would be able to get a `AccessToken a` because they
don't care about what you called `UserData` above.  However, some
other functions (such as isValid) do care about that and would need
`Either (AccessToken AppData) (AccessToken UserData)`.

That's not to say that we *couldn't* avoid GADTs.  We certainly could.
 But GADTs allow us to have our cake and eat it, too =).

Cheers,

--

-- 
Felipe.
Christian Maeder | 15 Aug 18:27 2012
Picon

Re: GADTs in the wild

Am 15.08.2012 17:58, schrieb Felipe Almeida Lessa:
> On Wed, Aug 15, 2012 at 12:54 PM, Christian Maeder
> <Christian.Maeder <at> dfki.de> wrote:
>> Well, "Either" was an adhoc choice and should be application specific.
>> Another h98 solution would be to keep the common part in a single
>> constructor:
>>
>>    data UserOrAppData = AppData | UserData UserId UTCTime
>>    data AccessToken = AccessToken UserOrAppData AccessTokenData
>
> This is a non-solution since you can't specify anymore that you want
> an user access token but not an app access token.
>
>> or: data AccessToken a = AccessToken a AccessTokenData
>
> And this one brings us the Either again (although on fewer places).
> Most functions would be able to get a `AccessToken a` because they
> don't care about what you called `UserData` above.  However, some
> other functions (such as isValid) do care about that and would need
> `Either (AccessToken AppData) (AccessToken UserData)`.

This type does not share the AccessTokenData and corresponds to 
"AccessToken UserOrAppData".

>
> That's not to say that we *couldn't* avoid GADTs.  We certainly could.
>   But GADTs allow us to have our cake and eat it, too =).

Sure, but portability is a value, too.

C.

>
> Cheers,
>
Edward Kmett | 14 Aug 16:32 2012
Picon

Re: GADTs in the wild

We use a form of stream transducer here at Capital IQ that uses GADTs, kind polymorphism and data kinds:


data SF k a b
  = Emit b (SF k a b)
  | Receive (k a (SF k a b))

data Fork :: (*,*) -> * -> * where
  L :: (a -> c) -> Fork '(a, b) c
  R :: (b -> c) -> Fork '(a, b) c

type Pipe = SF (->)
type Tee a b = SF Fork '(a, b)

instance Category (SF (->)) where
  id = arr id
  Emit a as . sf = Emit a (as . sf)
  Receive f . Emit b bs = f b . bs
  sf . Receive g = Receive (\a -> sf . g a)

arr :: (a -> b) -> Pipe a b
arr f = z where
  loop a = Emit (f a) z
  z = Receive loop

repeat :: b -> SF k a b
repeat b = Emit b z
  where z = repeat b

filter :: (a -> Bool) -> Pipe a a
filter p = z
  where loop a | p a = Emit a z
               | otherwise = z
        z = Receive loop

You can extend the model to support non-deterministic read from whichever input is available with

data NonDetFork :: (*,*) -> * -> * where
  NDL :: (a -> c) -> NonDetFork '(a, b) c
  NDR :: (b -> c) -> NonDetFork '(a, b) c
  NDB :: (a -> b) -> (b -> c) -> NonDetFork '(a, b) c

These could admittedly be implemented using a more traditional GADT without poly/data kinds, by just using (a,b) instead of '(a,b), though.

-Edward Kmett

On Tue, Aug 14, 2012 at 7:32 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

Friends


I’m giving a series of five lectures at the Laser Summer School (2-8 Sept), on “Adventures with types in Haskell”.  My plan is:

1.   Type classes

2.   Type families [examples including Repa type tags]

3.   GADTs

4.   Kind polymorphism

5.   System FC and deferred type errors

 

This message is to invite you to send me your favourite example of using a GADT to get the job done.  Ideally I’d like to use examples that are (a) realistic, drawn from practice (b) compelling and (c) easy to present without a lot of background.  Most academic papers only have rather limited examples, usually eval :: Term t -> t, but I know that GADTs are widely used in practice.

 

Any ideas from your experience, satisfying (a-c)?  If so, and you can spare the time, do send me a short write-up. Copy the list, so that we can all benefit.

 

Many thanks


Simon


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 14 Aug 16:34 2012
Picon

Re: GADTs in the wild

On Tue, Aug 14, 2012 at 10:32 AM, Edward Kmett <ekmett <at> gmail.com> wrote:

data NonDetFork :: (*,*) -> * -> * where
  NDL :: (a -> c) -> NonDetFork '(a, b) c
  NDR :: (b -> c) -> NonDetFork '(a, b) c
  NDB :: (a -> b) -> (b -> c) -> NonDetFork '(a, b) c
er..
  NDB :: (a -> c) -> (b -> c) -> NonDetFork '(a, b) c

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Gábor Lehel | 14 Aug 20:43 2012
Picon

Re: GADTs in the wild

Lennart Augustsson has a really interesting example of using GADTs and
the Maybe monad to validate an untyped AST into a typed,
(mostly-)correct-by-construction AST here:

http://augustss.blogspot.com/2009/06/more-llvm-recently-someone-asked-me-on.html

This was one of my first exposures to GADTs and it set my mind racing.
I wrote a small compiler for simple scalar/vector/matrix arithmetic
expressions with variables as my first nontrivial Haskell project, and
it was heavily inspired by Lennart's article. (I can put it up online
if anyone's interested, but I'm not relishing the thought of updating
LLVM on my system and the various packages and possibly the code to
make it all work again.)

On Tue, Aug 14, 2012 at 1:32 PM, Simon Peyton-Jones
<simonpj <at> microsoft.com> wrote:
> Friends
>
>
> I’m giving a series of five lectures at the Laser Summer School (2-8 Sept),
> on “Adventures with types in Haskell”.  My plan is:
>
> 1.   Type classes
>
> 2.   Type families [examples including Repa type tags]
>
> 3.   GADTs
>
> 4.   Kind polymorphism
>
> 5.   System FC and deferred type errors
>
>
>
> This message is to invite you to send me your favourite example of using a
> GADT to get the job done.  Ideally I’d like to use examples that are (a)
> realistic, drawn from practice (b) compelling and (c) easy to present
> without a lot of background.  Most academic papers only have rather limited
> examples, usually eval :: Term t -> t, but I know that GADTs are widely used
> in practice.
>
>
>
> Any ideas from your experience, satisfying (a-c)?  If so, and you can spare
> the time, do send me a short write-up. Copy the list, so that we can all
> benefit.
>
>
>
> Many thanks
>
>
> Simon
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users <at> haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>

--

-- 
Your ship was destroyed in a monadic eruption.
Roman Cheplyaka | 14 Aug 23:22 2012

Re: GADTs in the wild

* Simon Peyton-Jones <simonpj <at> microsoft.com> [2012-08-14 11:32:19+0000]
> This message is to invite you to send me your favourite example of
> using a GADT to get the job done.  Ideally I'd like to use examples
> that are (a) realistic, drawn from practice (b) compelling and (c)
> easy to present without a lot of background.  Most academic papers
> only have rather limited examples, usually eval :: Term t -> t, but I
> know that GADTs are widely used in practice.
> 
> Any ideas from your experience, satisfying (a-c)?  If so, and you can
> spare the time, do send me a short write-up. Copy the list, so that we
> can all benefit.

Here's how you can encode regular expressions as a GADT:

data RE s a where
    Eps :: RE s ()
    Sym :: (s -> Bool) -> RE s s
    Alt :: RE s a -> RE s b -> RE s (Either a b)
    Seq :: RE s a -> RE s b -> RE s (a, b)
    Rep :: RE s a -> RE s [a]

If you add one more constructor, Fmap :: (a -> b) -> RE s a -> RE s b,
RE will become Functor and Applicative (and half-Alternative).

This is a simplified extract from the regex-applicative library:
https://github.com/feuerbach/regex-applicative/blob/master/Text/Regex/Applicative/Types.hs#L58

--

-- 
Roman I. Cheplyaka :: http://ro-che.info/
Manuel M T Chakravarty | 15 Aug 04:52 2012
Picon
Picon

Re: GADTs in the wild

Most academic papers do use the eval example, but it is a practical example. This use of GADTs is nice for embedded languages. For example, Accelerate uses a supercharged version of it to catch as many errors as possible during Haskell host program compile-time (as opposed to Accelerate compile time, which is Haskell runtime).

Manuel


Simon Peyton-Jones <simonpj <at> microsoft.com>:
Friends


I’m giving a series of five lectures at the Laser Summer School (2-8 Sept), on “Adventures with types in Haskell”.  My plan is:

1.   Type classes

2.   Type families [examples including Repa type tags]

3.   GADTs

4.   Kind polymorphism

5.   System FC and deferred type errors

 
This message is to invite you to send me your favourite example of using a GADT to get the job done.  Ideally I’d like to use examples that are (a) realistic, drawn from practice (b) compelling and (c) easy to present without a lot of background.  Most academic papers only have rather limited examples, usually eval :: Term t -> t, but I know that GADTs are widely used in practice.

 
Any ideas from your experience, satisfying (a-c)?  If so, and you can spare the time, do send me a short write-up. Copy the list, so that we can all benefit.

 
Many thanks


Simon

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Yitzchak Gale | 15 Aug 23:13 2012

Re: GADTs in the wild

Simon Peyton-Jones wrote:
> This message is to invite you to send me your favourite example of using a
> GADT to get the job done.  Ideally I’d like to use examples that are (a)
> realistic, drawn from practice (b) compelling and (c) easy to present
> without a lot of background.

Last year I presented the following simple puzzle to the
community:

http://www.haskell.org/pipermail/haskell-cafe/2011-February/089719.html

That puzzle actually came up in a real-life software project
in Haskell that I was working on.

Several solutions were submitted that used various
Haskell extensions such as rank N types and generics,
as well as a rather cumbersome Haskell 98 solution.

But in my opinion, by far the best solution, using only
GADTs, was submitted by Eric Mertens:

http://hpaste.org/44469/software_stack_puzzle

Eric's solution could now be simplified even further
using data kinds.

Yitz
Christian Maeder | 17 Aug 12:59 2012
Picon

Re: GADTs in the wild

Am 15.08.2012 23:13, schrieb Yitzchak Gale:
> But in my opinion, by far the best solution, using only
> GADTs, was submitted by Eric Mertens:
>
> http://hpaste.org/44469/software_stack_puzzle
>
> Eric's solution could now be simplified even further
> using data kinds.

Find attached a version (based on Eric's solution) that uses only 
ExistentialQuantification.

data Fun a c = First (a -> c)
   | forall b . Serializable b => Fun b c :. (a -> b)

instead of:

data Fun :: * -> * -> * where
    Id   :: Fun a a
    (:.) :: Serializable b => Fun b c -> (a -> b) -> Fun a c

The main problem seems to be to create a dependently typed list of 
functions (the type of the next element depends on the previous one)
For such a list the element type depends on the index, therefore it 
seems not possible to define take and drop over "Fun a c" and compose it 
like

   serialize . flatten (take n fs) . deserialize

(as would be easily possible with functions of type "a -> a")

Cheers Christian

>
> Yitz
>

Attachment (Puzzle.hs): text/x-haskell, 1701 bytes
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
José Pedro Magalhães | 16 Aug 10:16 2012
Picon

Re: GADTs in the wild

Simon,

We rely extensively on GADTs for modelling musical harmony in HarmTrace:

PDF: http://www.dreixel.net/research/pdf/fmmh.pdf
Hackage: http://hackage.haskell.org/package/HarmTrace

Not entirely sure it passes (c), though.


Cheers,
Pedro

On Tue, Aug 14, 2012 at 1:32 PM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

Friends


I’m giving a series of five lectures at the Laser Summer School (2-8 Sept), on “Adventures with types in Haskell”.  My plan is:

1.   Type classes

2.   Type families [examples including Repa type tags]

3.   GADTs

4.   Kind polymorphism

5.   System FC and deferred type errors

 

This message is to invite you to send me your favourite example of using a GADT to get the job done.  Ideally I’d like to use examples that are (a) realistic, drawn from practice (b) compelling and (c) easy to present without a lot of background.  Most academic papers only have rather limited examples, usually eval :: Term t -> t, but I know that GADTs are widely used in practice.

 

Any ideas from your experience, satisfying (a-c)?  If so, and you can spare the time, do send me a short write-up. Copy the list, so that we can all benefit.

 

Many thanks


Simon


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Christopher Done | 17 Aug 15:14 2012
Picon

Re: GADTs in the wild

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.

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Christopher Done | 17 Aug 15:37 2012
Picon

Re: GADTs in the wild

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.

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Felipe Almeida Lessa | 17 Aug 17:56 2012
Picon

Re: GADTs in the wild

Christopher, did you ever take a look at acid-state [1]?  It seems to
me that it solves the same problem you have but, instead of

  Client <-> JSON <-> Server (going through the web)

it solves

  Server <-> Storage <-> Server (going through time)

Cheers,

[1] http://hackage.haskell.org/package/acid-state

--

-- 
Felipe.
Bertram Felgenhauer | 18 Aug 20:57 2012

Re: GADTs in the wild

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.

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Christopher Done | 18 Aug 21:23 2012
Picon

Re: GADTs in the wild

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. 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.
Bertram Felgenhauer | 18 Aug 22:05 2012

Re: GADTs in the wild

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
Scott Michel | 23 Aug 20:47 2012
Picon

Re: GADTs in the wild

Here's an example (not a complete module) I was using to represent bit-oriented structures as they occur in certain space applications, notably GPS frames. "Fixed" allows for fixed-sized fields and lets the end user choose the integral type that's best for the structure.

At least it's not a parser or language example. :-)


-scooter

-- | Member fields, etc., that comprise a 'BitStruct'
data Member where
  Field    :: String                    -- Field name
              -> Int                    -- Field length
              -> Bool                   -- Signed (True) or unsigned (False)
              -> Member
  ZeroPad  :: String                    -- Field name
              -> Int                    -- Field length
              -> Member
  OnesPad  :: String                    -- Field name
              -> Int                    -- Field length
              -> Member
  ArbPad   :: String                    -- Field name
              -> Int                    -- Field length
              -> Member
  Reserved :: String                    -- Field name
              -> Int                    -- Field length
              -> Member
  Fixed    :: (Integral x, Show x) =>
              String                    -- Field name
              -> Int                    -- Field length
              -> Bool                   -- Signed (True) or unsigned (False)
              -> x                      -- Type of the fixed field's value
              -> Member
  Variant  :: (Integral x, Show x) =>
              String                    -- Variant prefix name
              -> Maybe BitStruct        -- Header before the tag
              -> TagElement             -- The tag element itself
              -> Maybe BitStruct        -- Common elements after the tag
              -> Seq (x, BitStruct)     -- Variant element tuples (value, structure)
              -> Member
  -- Mult-value variant: Use this when multiple variant tag values have the
  -- same structure:
  MultiValueVariant :: (Integral x, Show x) =>
              String                            -- Variant prefix name
              -> Maybe BitStruct                -- Header before the tag
              -> TagElement                     -- The tag element itself
              -> Maybe BitStruct                -- Common elements after the tag
              -> Seq ([x], BitStruct)           -- Variant element tuples ([values], structure)
              -> Member

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Scott Michel | 23 Aug 20:50 2012
Picon

Re: GADTs in the wild

Probably useful to include a "mkFixed" function example as well, to show how a Fixed can be constructed using the "optimal" data representation:

-- | Make a fixed field.
--
-- Note that this type constructor function chooses the minimal type
-- representation for the fixed value stored. Unsigned representations
-- are preferred over signed.
mkFixed :: String -> Int -> Integer -> Member
mkFixed name len val
  | len <= 0  = error $ "mkFixed " ++ name ++ ": length < 0"
  | len < 8  && validUnsigned len val = Fixed name len False (fromIntegral val :: Word8)
  | len < 8  && validSigned   len val = Fixed name len True  (fromIntegral val :: Int8)
  | len < 16 && validUnsigned len val = Fixed name len False (fromIntegral val :: Word16)
  | len < 16 && validSigned   len val = Fixed name len True  (fromIntegral val :: Int16)
  | len < 32 && validUnsigned len val = Fixed name len False (fromIntegral val :: Word32)
  | len < 32 && validSigned   len val = Fixed name len True  (fromIntegral val :: Int32)
  | len < 64 && validUnsigned len val = Fixed name len False (fromIntegral val :: Word64)
  | len < 64 && validSigned   len val = Fixed name len True  (fromIntegral val :: Int64)
  | otherwise = error $ "mkFixed " ++ name ++ ": cannot represent this bit field"


On Thu, Aug 23, 2012 at 11:47 AM, Scott Michel <scooter.phd <at> gmail.com> wrote:
Here's an example (not a complete module) I was using to represent bit-oriented structures as they occur in certain space applications, notably GPS frames. "Fixed" allows for fixed-sized fields and lets the end user choose the integral type that's best for the structure.

At least it's not a parser or language example. :-)


-scooter

-- | Member fields, etc., that comprise a 'BitStruct'
data Member where
  Field    :: String                    -- Field name
              -> Int                    -- Field length
              -> Bool                   -- Signed (True) or unsigned (False)
              -> Member
  ZeroPad  :: String                    -- Field name
              -> Int                    -- Field length
              -> Member
  OnesPad  :: String                    -- Field name
              -> Int                    -- Field length
              -> Member
  ArbPad   :: String                    -- Field name
              -> Int                    -- Field length
              -> Member
  Reserved :: String                    -- Field name
              -> Int                    -- Field length
              -> Member
  Fixed    :: (Integral x, Show x) =>
              String                    -- Field name
              -> Int                    -- Field length
              -> Bool                   -- Signed (True) or unsigned (False)
              -> x                      -- Type of the fixed field's value
              -> Member
  Variant  :: (Integral x, Show x) =>
              String                    -- Variant prefix name
              -> Maybe BitStruct        -- Header before the tag
              -> TagElement             -- The tag element itself
              -> Maybe BitStruct        -- Common elements after the tag
              -> Seq (x, BitStruct)     -- Variant element tuples (value, structure)
              -> Member
  -- Mult-value variant: Use this when multiple variant tag values have the
  -- same structure:
  MultiValueVariant :: (Integral x, Show x) =>
              String                            -- Variant prefix name
              -> Maybe BitStruct                -- Header before the tag
              -> TagElement                     -- The tag element itself
              -> Maybe BitStruct                -- Common elements after the tag
              -> Seq ([x], BitStruct)           -- Variant element tuples ([values], structure)
              -> Member


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane