4 ms·

BTW, if any HN readers have good practical examples of GADT I'd love to hear them. The article does a fine job of explaining the advantages GADT give but real w

by ufo 12y ago

BTW, if any HN readers have good practical examples of GADT I'd love to hear them. The article does a fine job of explaining the advantages GADT give but real world examples would greatly complement that. Also, has anyone ever used gadts to implement type safe syntax trees like that? Last time I implemented a little programming language I used regular ADTs and had a separate type-checking pass to verify that everything is all right. I don't know how hard it would be to write a gadt version of my ast and if it would be worth the trouble.

lpw25 12y ago
> Also, has anyone ever used gadts to implement type safe syntax trees like that? I believe the main use is for embedded DSLs. I'm afraid I don't have any practical examples on hand to link to.
- moomin 12y ago
  Consider an HTTP request. A get can't have a body, a post can. So you could define data Request b where GET :: Headers -> Request () POST :: Headers -> body -> Request body As the article says, building up your intuition is the hard bit. You could go further by typing the headers to recognize the type of body you're dealing with.
Martijn 12y ago
My Magic: the Gathering implementation uses a few GADTs. Interestingly they use GADTs in very different ways. Source code is here: https://github.com/MedeaMelana/Magic/blob/master/Magic/src/Magic/Types.hs https://github.com/MedeaMelana/Magic/blob/master/Magic/src/M... Let me briefly highlight three of them: 1) Type Question models questions that the game might ask of players. Its constructors are tagged with the type of the answer to that question: data Question a where AskKeepHand :: Question Bool AskTarget :: [EntityRef] -> Question EntityRef ... This allows me to write cards that ask questions and later on plug in various interpreters of these questions (command line interface, JSON webserver, AI, test framework). 2) The ZoneRef datatype enumerates the various zones in a game of Magic (battlefield, hand, etc) but I've chosen to tag each ZoneRef constructor with a type that indicates what the type of a card is when you look up a reference to a card ("object" in Magic jargon): type ObjectRef ty = (ZoneRef ty, Id) lookupObject :: ObjectRef ty -> Magic (ObjectOfType ty) Most functions that take object references as an argument like to constrain the type of the object referenced, and using a GADT allows them to do so. For example, dealing damage to an object (creature or planeswalker): data SimpleOneShotEffect = DamageObject Object (ObjectRef TyPermanent) Int ... 3) Type TargetList models zero or more targets a spell on the stack can target. Even though in essence it is just a list of targets, it is a GADT so that it can have a "return type" which is re-evaluated when one of more of the targets change (for example, by a card like Redirect or Reverberate). Hope this helps!
- ufo 12y ago
  What an interesting example. Not what I was expecting! Can you think of an example of a bug that you avoided due to the extra type safety of gadts? Magic has some pretty complex rules so I imagine that writing exaustive test must be hard and that the extra static guarantees might be able to find something a dynamic checker wouldn't. (Its ok if you need some ingame jargon to explain that, I know the basic rules).
  - Martijn 12y ago
    It's a combination of avoiding potential bugs and just modelling things differently altogether: If I had to leave out the answer type of questions, I'd have to come up with an entirely different way of modelling answers. For example, I might have had to write a datatype like: data Answer = AnswerBool Bool | AnswerInt Int | ... and then processing the answer (through pattern matching) would have to discard any answer it didn't like, which is awkward. Or I would have had to use a type class to keep everything type-safe which would have resulted in more complicated type signatures throughout the code. For the TargetList, the current setup allows me to write functions that consume a target list of exactly the right size, for example: \(target1, target2) -> ... rather than a normal list: \[target1, target2] -> ... which in this case results in a pattern match exception if you pass it a list of any length other than 2.
tel 12y ago
I use them all the time for little EDSLs in Haskell. They also go really nicely when implementing AFRP libraries. You can also do a lot with them and type families for making typed APIs. Oliver Charles has some work doing this over websockets for instance: https://skillsmatter.com/skillscasts/5356-oliver-charles https://skillsmatter.com/skillscasts/5356-oliver-charles
- lomnakkus 12y ago
  That video doesn't appear to available to everyone. It says "Sorry Because of its privacy settings, this video cannot be played here." Not sure if it's because of country/IP restrictions or what.
  - tel 12y ago
    I thought Ollie had a blog post about this stuff somewhere, but I can't find it now. He does other things which involve fairly advanced GADT work, though https://ocharles.org.uk/blog/posts/2014-06-10-reversible-serialization.html https://ocharles.org.uk/blog/posts/2014-06-10-reversible-ser...
MaxScheiber 12y ago
http://www.seas.upenn.edu/~cis552/lectures/RedBlackGADT1.html http://www.seas.upenn.edu/~cis552/lectures/RedBlackGADT1.htm... Red-black trees via GADTs, courtesy of Penn's CIS 552 course.
Peaker 12y ago
https://github.com/yairchu/red-black-tree https://github.com/yairchu/red-black-tree Has implementations of some binary search trees with GADTs to guarantee, at compile-time, that most of the tree's invariants always hold.
avsm 12y ago
The Mirage OS configuration languages use them to provide a safe interface between device driver descriptions and module implementations. The core is as simple as: type _ typ = | Type: 'a -> 'a typ | Function: 'a typ * 'b typ -> ('a -> 'b) typ From https://github.com/mirage/mirage/blob/master/lib/mirage.ml#L67 https://github.com/mirage/mirage/blob/master/lib/mirage.ml#L... I talked about this usecase in the ML Workshop in ICFP this year; video here: https://www.youtube.com/watch?v=oKJ8Sxqr4r8 https://www.youtube.com/watch?v=oKJ8Sxqr4r8 Some blog posts here: http://openmirage.org/blog/intro-tcpip http://openmirage.org/blog/intro-tcpip
toolslive 12y ago
we use it to create a remote procedure call serialization protocol. (in essence, this is an interpreter too)

by ufo 12y ago

lpw25 12y ago

> Also, has anyone ever used gadts to implement type safe syntax trees like that? I believe the main use is for embedded DSLs. I'm afraid I don't have any practical examples on hand to link to.

moomin 12y ago
Consider an HTTP request. A get can't have a body, a post can. So you could define data Request b where GET :: Headers -> Request () POST :: Headers -> body -> Request body As the article says, building up your intuition is the hard bit. You could go further by typing the headers to recognize the type of body you're dealing with.

Martijn 12y ago

My Magic: the Gathering implementation uses a few GADTs. Interestingly they use GADTs in very different ways. Source code is here: https://github.com/MedeaMelana/Magic/blob/master/Magic/src/Magic/Types.hs https://github.com/MedeaMelana/Magic/blob/master/Magic/src/M... Let me briefly highlight three of them: 1) Type Question models questions that the game might ask of players. Its constructors are tagged with the type of the answer to that question: data Question a where AskKeepHand :: Question Bool AskTarget :: [EntityRef] -> Question EntityRef ... This allows me to write cards that ask questions and later on plug in various interpreters of these questions (command line interface, JSON webserver, AI, test framework). 2) The ZoneRef datatype enumerates the various zones in a game of Magic (battlefield, hand, etc) but I've chosen to tag each ZoneRef constructor with a type that indicates what the type of a card is when you look up a reference to a card ("object" in Magic jargon): type ObjectRef ty = (ZoneRef ty, Id) lookupObject :: ObjectRef ty -> Magic (ObjectOfType ty) Most functions that take object references as an argument like to constrain the type of the object referenced, and using a GADT allows them to do so. For example, dealing damage to an object (creature or planeswalker): data SimpleOneShotEffect = DamageObject Object (ObjectRef TyPermanent) Int ... 3) Type TargetList models zero or more targets a spell on the stack can target. Even though in essence it is just a list of targets, it is a GADT so that it can have a "return type" which is re-evaluated when one of more of the targets change (for example, by a card like Redirect or Reverberate). Hope this helps!

ufo 12y ago
What an interesting example. Not what I was expecting! Can you think of an example of a bug that you avoided due to the extra type safety of gadts? Magic has some pretty complex rules so I imagine that writing exaustive test must be hard and that the extra static guarantees might be able to find something a dynamic checker wouldn't. (Its ok if you need some ingame jargon to explain that, I know the basic rules).
- Martijn 12y ago
  It's a combination of avoiding potential bugs and just modelling things differently altogether: If I had to leave out the answer type of questions, I'd have to come up with an entirely different way of modelling answers. For example, I might have had to write a datatype like: data Answer = AnswerBool Bool | AnswerInt Int | ... and then processing the answer (through pattern matching) would have to discard any answer it didn't like, which is awkward. Or I would have had to use a type class to keep everything type-safe which would have resulted in more complicated type signatures throughout the code. For the TargetList, the current setup allows me to write functions that consume a target list of exactly the right size, for example: \(target1, target2) -> ... rather than a normal list: \[target1, target2] -> ... which in this case results in a pattern match exception if you pass it a list of any length other than 2.

tel 12y ago

I use them all the time for little EDSLs in Haskell. They also go really nicely when implementing AFRP libraries. You can also do a lot with them and type families for making typed APIs. Oliver Charles has some work doing this over websockets for instance: https://skillsmatter.com/skillscasts/5356-oliver-charles https://skillsmatter.com/skillscasts/5356-oliver-charles

lomnakkus 12y ago
That video doesn't appear to available to everyone. It says "Sorry Because of its privacy settings, this video cannot be played here." Not sure if it's because of country/IP restrictions or what.
- tel 12y ago
  I thought Ollie had a blog post about this stuff somewhere, but I can't find it now. He does other things which involve fairly advanced GADT work, though https://ocharles.org.uk/blog/posts/2014-06-10-reversible-serialization.html https://ocharles.org.uk/blog/posts/2014-06-10-reversible-ser...

MaxScheiber 12y ago

http://www.seas.upenn.edu/~cis552/lectures/RedBlackGADT1.html http://www.seas.upenn.edu/~cis552/lectures/RedBlackGADT1.htm... Red-black trees via GADTs, courtesy of Penn's CIS 552 course.

Peaker 12y ago

https://github.com/yairchu/red-black-tree https://github.com/yairchu/red-black-tree Has implementations of some binary search trees with GADTs to guarantee, at compile-time, that most of the tree's invariants always hold.

avsm 12y ago

The Mirage OS configuration languages use them to provide a safe interface between device driver descriptions and module implementations. The core is as simple as: type _ typ = | Type: 'a -> 'a typ | Function: 'a typ * 'b typ -> ('a -> 'b) typ From https://github.com/mirage/mirage/blob/master/lib/mirage.ml#L67 https://github.com/mirage/mirage/blob/master/lib/mirage.ml#L... I talked about this usecase in the ML Workshop in ICFP this year; video here: https://www.youtube.com/watch?v=oKJ8Sxqr4r8 https://www.youtube.com/watch?v=oKJ8Sxqr4r8 Some blog posts here: http://openmirage.org/blog/intro-tcpip http://openmirage.org/blog/intro-tcpip

toolslive 12y ago

we use it to create a remote procedure call serialization protocol. (in essence, this is an interpreter too)