3 ms·
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 bo
by 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 agoWell 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 agoThe 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.
- tel 12y agoYou 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.