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.

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 :

...

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, =)

Am 15.08.2012 17:58, schrieb Felipe Almeida Lessa:

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

On Tue, Aug 14, 2012 at 10:32 AM, Edward Kmett 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

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

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.

Christopher Done wrote:

On 18 August 2012 20:57, Bertram Felgenhauer wrote:

...

The natural encoding as a GADT would be as follows:

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

Right, that's exactly what I wrote at the end of my email.

Sorry, I missed that.

And then indeed dispatch would be `dispatch :: Command a -> Snap a`. But how do you derive an instance of Typeable and Read for this data type? The Foo and the Double conflict and give a type error.

Right. A useful Read instance can't be implemented at all for the GADT. I'm unsure about Typeable. You have to provide the instances for the existential wrapper (SerializableCommand) instead, which defeats automatic deriving. And this wrapper almost isomorphic to the non-GADT Command type that you ended up using. So the trade-off is between some loss of type safety and having to write boilerplate code. The obvious question then is how to automate the boilerplate code generation. In principle, Template Haskell is equipped to deal with GADTs, but I see little existing work in this direction. There is derive-gadt on hackage, but at a glance the code is a mess and the main idea seems to be to provide separate instances for each possible combination of type constructor and type argument. (So there would be two Read instances for the type above, Read (Command Foo) and Read (Command Double)), which is going in the wrong direction. I suspect that the code will not be useful. Is there anything else? Best regards, Bertram

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 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