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
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 ;;