15 ms·

Detecting use cases for GADTs in OCaml

53 points by mads_hartmann 12y ago

wk_end 12y ago
Unless I'm misreading this, there's a slight semantic difference between the two cases: with the GADT-based interpreter, an if expression's two branches must both evaluate to integers: | GIf : bool expr' * int expr' * int expr' -> int expr' ...whereas in the original both branches could evaluate to bools (or even totally separate types). Do you need a separate case for each type, or could one write something like the following? | GIf : bool expr' * a expr' * a expr' -> a expr'
- mads_hartmann 12y ago
  Well spotted, you're absolutely right. My hunch is that it's doable to maintain the semantics but I need to play around with the example a bit to know for sure.
- mads_hartmann 12y ago
  The following implementation comes closer to the original semantics of the ADT implementation. type _ value' = | GBool : bool -> bool value' | GInt : int -> int value' type _ expr' = | GValue : 'a value' -> 'a expr' | GIf : bool expr' * 'a expr' * 'a expr' -> 'a expr' | GEq : 'a expr' * 'a expr' -> bool expr' | GLt : int expr' * int expr' -> bool expr' let rec eval' : type a. a expr' -> a = function | GValue (GBool b) -> b | GValue (GInt i) -> i | GIf (b, l, r) -> if eval' b then eval' l else eval' r | GEq (a, b) -> (eval' a) = (eval' b) | GLt (a,b) -> a < b ;; eval' (GIf ((GEq ((GValue (GInt 2)), (GValue (GInt 2)))), (GValue (GInt 42)), (GValue (GInt 12))));; eval' (GIf ((GEq ((GValue (GInt 2)), (GValue (GInt 2)))), (GValue (GBool true)), (GValue (GBool false))));; It does not support having separate return types for the branches on an if-statement but I consider that to be a good thing ;) I should probably update the ADT example to dis-allow that.
  - nhaehnle 12y ago
    It should still be possible to simplify eval' by merging the two GValue cases, right?
    - tel 12y ago
      As long as you're okay with your DSL subsiding all OCaml types you can do GLift : a -> a expr'
    - mercurial 12y ago
      I don't think you can do that since the wrapped values have different types.
- tel 12y ago
  You can think of GADTs as generating equalities when you match on a constructor. So when you open up `GIf(c, t, e)` you'll find c : vc expr' t : vt expr' e : ve expr' with an ambient type variable `a` and proofs of type equalities vc ~ bool vt ~ a ve ~ a When you solve those equations they'll work for any choices of `a` so long as `vt` and `ve` both can unify with it.
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!
kxyvr 12y ago
In the past, I've used them to eliminate and optimize branches with simple interpreters. That being said, I've had better luck with using things like Coq to write a certified interpreter and then outputing to OCaml. In any case, when we write a simple interpreter for a typed language, we normally run things through a type checker first and then evaluate it. After type checking, we know that certain errors can not occur, such as adding an integer to a boolean, but this information gets lost when passing everything to the evaluator. As far as the evaluator knows, all we have are expressions, so we still have to check for situations like adding an integer to a boolean in the evaluator. Again, this can not occur because we type checked everything, but these branches are necessary to have the OCaml compiler type check everything. What GADTs allow is for the type checker to translate an expression into a typed expression and then the evaluator translates a typed expression into a value. This eliminates these redundant branches. For some sample code, I wrote about this on StackOverflow some time back. The following link contains both a traditional implementation of an OCaml interpreter as well as one that uses GADTs. It differs some from the one in the article because I work out how to make this work with an environment, lambda functions, and closures: https://stackoverflow.com/questions/22676975/simple-lambda-calculus-dsl-using-gadts-in-ocaml https://stackoverflow.com/questions/22676975/simple-lambda-c...

53 points by mads_hartmann 12y ago

Unless I'm misreading this, there's a slight semantic difference between the two cases: with the GADT-based interpreter, an if expression's two branches must both evaluate to integers: | GIf : bool expr' * int expr' * int expr' -> int expr' ...whereas in the original both branches could evaluate to bools (or even totally separate types). Do you need a separate case for each type, or could one write something like the following? | GIf : bool expr' * a expr' * a expr' -> a expr'

mads_hartmann 12y ago
Well spotted, you're absolutely right. My hunch is that it's doable to maintain the semantics but I need to play around with the example a bit to know for sure.
mads_hartmann 12y ago
The following implementation comes closer to the original semantics of the ADT implementation. type _ value' = | GBool : bool -> bool value' | GInt : int -> int value' type _ expr' = | GValue : 'a value' -> 'a expr' | GIf : bool expr' * 'a expr' * 'a expr' -> 'a expr' | GEq : 'a expr' * 'a expr' -> bool expr' | GLt : int expr' * int expr' -> bool expr' let rec eval' : type a. a expr' -> a = function | GValue (GBool b) -> b | GValue (GInt i) -> i | GIf (b, l, r) -> if eval' b then eval' l else eval' r | GEq (a, b) -> (eval' a) = (eval' b) | GLt (a,b) -> a < b ;; eval' (GIf ((GEq ((GValue (GInt 2)), (GValue (GInt 2)))), (GValue (GInt 42)), (GValue (GInt 12))));; eval' (GIf ((GEq ((GValue (GInt 2)), (GValue (GInt 2)))), (GValue (GBool true)), (GValue (GBool false))));; It does not support having separate return types for the branches on an if-statement but I consider that to be a good thing ;) I should probably update the ADT example to dis-allow that.
- nhaehnle 12y ago
  It should still be possible to simplify eval' by merging the two GValue cases, right?
  - tel 12y ago
    As long as you're okay with your DSL subsiding all OCaml types you can do GLift : a -> a expr'
  - mercurial 12y ago
    I don't think you can do that since the wrapped values have different types.
tel 12y ago
You can think of GADTs as generating equalities when you match on a constructor. So when you open up `GIf(c, t, e)` you'll find c : vc expr' t : vt expr' e : ve expr' with an ambient type variable `a` and proofs of type equalities vc ~ bool vt ~ a ve ~ a When you solve those equations they'll work for any choices of `a` so long as `vt` and `ve` both can unify with it.

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!

kxyvr 12y ago

In the past, I've used them to eliminate and optimize branches with simple interpreters. That being said, I've had better luck with using things like Coq to write a certified interpreter and then outputing to OCaml. In any case, when we write a simple interpreter for a typed language, we normally run things through a type checker first and then evaluate it. After type checking, we know that certain errors can not occur, such as adding an integer to a boolean, but this information gets lost when passing everything to the evaluator. As far as the evaluator knows, all we have are expressions, so we still have to check for situations like adding an integer to a boolean in the evaluator. Again, this can not occur because we type checked everything, but these branches are necessary to have the OCaml compiler type check everything. What GADTs allow is for the type checker to translate an expression into a typed expression and then the evaluator translates a typed expression into a value. This eliminates these redundant branches. For some sample code, I wrote about this on StackOverflow some time back. The following link contains both a traditional implementation of an OCaml interpreter as well as one that uses GADTs. It differs some from the one in the article because I work out how to make this work with an environment, lambda functions, and closures: https://stackoverflow.com/questions/22676975/simple-lambda-calculus-dsl-using-gadts-in-ocaml https://stackoverflow.com/questions/22676975/simple-lambda-c...