Re: GADTs in the wild

[Scott Michel]

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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Scott Michel]

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@gmail.comwrote:

 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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: 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.

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Christopher Done]

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

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Bertram Felgenhauer]

Christopher Done wrote:
 On 18 August 2012 20:57, Bertram Felgenhauer
 bertram.felgenha...@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

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Christian Maeder]

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



{-# LANGUAGE ExistentialQuantification #-}
module Puzzle where

import Data.ByteString (ByteString, singleton)

class Serializable a where
  serialize :: a - ByteString
  deserialize :: ByteString - a

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

infixl 9 :.

-- Simple conversion
flatten :: Fun a b - a - b
flatten (First f) = f
flatten (fs :. f) = flatten fs . f

-- Layering example
runLayers :: (Serializable a, Serializable b)
   = Int - Int - Fun a b - ByteString - ByteString
runLayers n m f = case f of
  fs :. _ | n  1 - runLayers (n - 1) (m - 1) fs
  _ - runLayers' m f . deserialize

runLayers' :: (Serializable a, Serializable b)
  = Int - Fun a b - a - ByteString
runLayers' m f = if m = 1 then serialize else case f of
  fs :. g - runLayers' (m - 1) fs . g
  First g - serialize . g

data Layer1 = Layer1
data Layer2 = Layer2
data Layer3 = Layer3
data Layer4 = Layer4

softwareStack :: Fun Layer1 Layer4
softwareStack =
  First (\ Layer3 - Layer4) :. (\ Layer2 - Layer3) :. (\ Layer1 - Layer2)

example1 = runLayers 2 4 softwareStack (singleton 2)  ==  singleton 4
example2 = runLayers 1 3 softwareStack (singleton 1)  ==  singleton 3

-- Boring serialization instances
instance Serializable Layer1 where
  serialize Layer1 = singleton 1
  deserialize bs | bs == singleton 1 = Layer1
instance Serializable Layer2 where
  serialize Layer2 = singleton 2
  deserialize bs | bs == singleton 2 = Layer2
instance Serializable Layer3 where
  serialize Layer3 = singleton 3
  deserialize bs | bs == singleton 3 = Layer3
instance Serializable Layer4 where
  serialize Layer4 = singleton 4
  deserialize bs | bs == singleton 4 = Layer4
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Christopher Done]

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.

Re: 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 chrisd...@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

Re: GADTs in the wild

[Felipe Almeida Lessa]

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.

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[José Pedro Magalhães]

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
simo...@microsoft.comwrote:

  Friends


 I’m giving a series of five lectures at the Laser Summer 
 Schoolhttp://laser.inf.ethz.ch/2012/(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@haskell.org
 http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Christian Maeder]

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.mae...@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, =)



___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Felipe Almeida Lessa]

On Wed, Aug 15, 2012 at 12:54 PM, Christian Maeder
christian.mae...@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.

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Christian Maeder]

Am 15.08.2012 17:58, schrieb Felipe Almeida Lessa:

On Wed, Aug 15, 2012 at 12:54 PM, Christian Maeder
christian.mae...@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,




___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Yitzchak Gale]

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

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Michael Snoyman]

On Tue, Aug 14, 2012 at 2:32 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:

  Friends


 I’m giving a series of five lectures at the Laser Summer 
 Schoolhttp://laser.inf.ethz.ch/2012/(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@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

[1]
https://docs.google.com/presentation/d/1c6pkskue6WbTlONFTpFhYqzSlQe_sxO7LfP5SW7InVE/edit
[2] http://hackage.haskell.org/package/groundhog
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Felipe Almeida Lessa]

On Tue, Aug 14, 2012 at 8:44 AM, Michael Snoyman mich...@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.

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Edward Kmett]

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
simo...@microsoft.comwrote:

  Friends


 I’m giving a series of five lectures at the Laser Summer 
 Schoolhttp://laser.inf.ethz.ch/2012/(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@haskell.org
 http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Edward Kmett]

On Tue, Aug 14, 2012 at 10:32 AM, Edward Kmett ekm...@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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Christian Maeder]

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.

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Felipe Almeida Lessa]

2012/8/14 Christian Maeder christian.mae...@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.

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Gábor Lehel]

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
simo...@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@haskell.org
 http://www.haskell.org/mailman/listinfo/glasgow-haskell-users




-- 
Your ship was destroyed in a monadic eruption.

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Roman Cheplyaka]

* Simon Peyton-Jones simo...@microsoft.com [2012-08-14 11:32:19+]
 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/

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs in the wild

[Manuel M T Chakravarty]

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 simo...@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@haskell.org
 http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users