Re: GADTs in the wild

2012-08-23 Thread 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

Re: GADTs in the wild

2012-08-23 Thread 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

Re: GADTs in the wild

2012-08-18 Thread 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)

Re: GADTs in the wild

2012-08-18 Thread 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

Re: GADTs in the wild

2012-08-18 Thread 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,

Re: GADTs in the wild

2012-08-17 Thread 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

Re: GADTs in the wild

2012-08-17 Thread 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

Re: GADTs in the wild

2012-08-17 Thread 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

Re: GADTs in the wild

2012-08-17 Thread 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]

Re: GADTs in the wild

2012-08-16 Thread 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

Re: GADTs in the wild

2012-08-15 Thread 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 =

Re: GADTs in the wild

2012-08-15 Thread 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

Re: GADTs in the wild

2012-08-15 Thread 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

Re: GADTs in the wild

2012-08-15 Thread 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

Re: GADTs in the wild

2012-08-14 Thread 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

Re: GADTs in the wild

2012-08-14 Thread 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

Re: GADTs in the wild

2012-08-14 Thread 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

Re: GADTs in the wild

2012-08-14 Thread 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,

Re: GADTs in the wild

2012-08-14 Thread 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

Re: GADTs in the wild

2012-08-14 Thread 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

Re: GADTs in the wild

2012-08-14 Thread 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

Re: GADTs in the wild

2012-08-14 Thread 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

Re: GADTs in the wild

2012-08-14 Thread 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