I’m trying to write a simple GADT-based evaluator for typed expressions, with the following expression variant:
type 'a expr =
| Int : int -> int expr
| Neg : int expr -> int expr
| Bool : bool -> bool expr
| Not : bool expr -> bool expr
I’d like to write a single eval : 'a expr -> 'a function that handles any expression type:
let rec eval (type a) (expr : a expr) : a =
match expr with
| Int n -> n
| Neg n -> - eval n
| Bool b -> b
| Not b -> not (eval b)
;;
This doesn’t compile, however. I get the following error (line 25 refers to the Not branch of the match):
File "main.ml", line 25, characters 24-25:
Error: This expression has type a expr but an expression was expected of type
int expr
Type a is not compatible with type int
Asking Merlin for the type of eval gives me int expr -> int, rather than 'a expr -> 'a, as I expected.
Is such an eval function even possible to write, or am I simply doing something wrong with type annotations or locally abstract types or something?
P.S. the following works fine, but is less satisfying:
let rec eval_bool (expr : bool expr) : bool =
match expr with
| Bool b -> b
| Not b -> not (eval_bool b)
and eval_int (expr : int expr) : int =
match expr with
| Int n -> n
| Neg n -> - eval_int n
;;