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
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
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)
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
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,
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
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
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
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]
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
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 =
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
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
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
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
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
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
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,
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
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
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
* 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
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
23 matches
Mail list logo