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.
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
...
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)
data SimpleOneShotEffect = DamageObject Object (ObjectRef TyPermanent) Int ...
Hope this helps!
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).
"Sorry
Because of its privacy settings, this video cannot be played here."
Not sure if it's because of country/IP restrictions or what.
The core is as simple as:
type _ typ =
| Type: 'a -> 'a typ
| Function: 'a typ * 'b typ -> ('a -> 'b) typ
I talked about this usecase in the ML Workshop in ICFP this year; video here: https://www.youtube.com/watch?v=oKJ8Sxqr4r8
Some blog posts here: http://openmirage.org/blog/intro-tcpip
Has implementations of some binary search trees with GADTs to guarantee, at compile-time, that most of the tree's invariants always hold.
Red-black trees via GADTs, courtesy of Penn's CIS 552 course.
I believe the main use is for embedded DSLs. I'm afraid I don't have any practical examples on hand to link to.
So you could define
data Request b where
GET :: Headers -> Request ()
POST :: Headers -> body -> Request body
You could go further by typing the headers to recognize the type of body you're dealing with.
| GIf : bool expr' * int expr' * int expr' -> int expr'
| GIf : bool expr' * a expr' * a expr' -> a expr' 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))));;
c : vc expr'
t : vt expr'
e : ve expr'
vc ~ bool
vt ~ a
ve ~ a
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-c...