Creating GADT expression in OCaml

Question

There is my toy GADT expression:

type _ expr =
  | Num : int -> int expr
  | Add : int expr * int expr -> int expr
  | Sub : int expr * int expr -> int expr
  | Mul : int expr * int expr -> int expr
  | Div : int expr * int expr -> int expr
  | Lt  : int expr * int expr -> bool expr
  | Gt  : int expr * int expr -> bool expr
  | And : bool expr * bool expr -> bool expr
  | Or  : bool expr * bool expr -> bool expr

Evaluation function:

let rec eval : type a. a expr -> a = function
  | Num n -> n
  | Add (a, b) -> (eval a) + (eval b)
  | Sub (a, b) -> (eval a) - (eval b)
  | Mul (a, b) -> (eval a) * (eval b)
  | Div (a, b) -> (eval a) / (eval b)
  | Lt  (a, b) -> (eval a) < (eval b)
  | Gt  (a, b) -> (eval a) > (eval b)
  | And (a, b) -> (eval a) && (eval b)
  | Or  (a, b) -> (eval a) || (eval b)

Creating expression is trivial when we limited to int expr:

let create_expr op a b =
  match op with
  | '+' -> Add (a, b)
  | '-' -> Sub (a, b)
  | '*' -> Mul (a, b)
  | '/' -> Div (a, b)
  | _ -> assert false

The question is how to support both int expr and bool expr in create_expr function.

My try:

type expr' = Int_expr of int expr | Bool_expr of bool expr

let concrete : type a. a expr -> expr' = function
  | Num _ as expr -> Int_expr expr
  | Add _ as expr -> Int_expr expr
  | Sub _ as expr -> Int_expr expr
  | Mul _ as expr -> Int_expr expr
  | Div _ as expr -> Int_expr expr
  | Lt  _ as expr -> Bool_expr expr
  | Gt  _ as expr -> Bool_expr expr
  | And _ as expr -> Bool_expr expr
  | Or  _ as expr -> Bool_expr expr

let create_expr (type a) op (a:a expr) (b:a expr) : a expr =
  match op, concrete a, concrete b with
  | '+', Int_expr  a, Int_expr  b -> Add (a, b)
  | '-', Int_expr  a, Int_expr  b -> Sub (a, b)
  | '*', Int_expr  a, Int_expr  b -> Mul (a, b)
  | '/', Int_expr  a, Int_expr  b -> Div (a, b)
  | '<', Int_expr  a, Int_expr  b -> Lt  (a, b)
  | '>', Int_expr  a, Int_expr  b -> Gt  (a, b)
  | '&', Bool_expr a, Bool_expr b -> And (a, b)
  | '|', Bool_expr a, Bool_expr b -> Or  (a, b)
  | _ -> assert false

It still can't return value of generalized type.

Error: This expression has type int expr but an expression was expected of type a expr Type int is not compatible with type a

UPDATE

Thanks to @gsg, I was able to implement type safe evaluator. Two tricks are crucial there:

• existential wrapper Any
• type tagging (TyInt and TyBool) that lets us to pattern match Any type

see

type _ ty =
  | TyInt : int ty
  | TyBool : bool ty

type any_expr = Any : 'a ty * 'a expr -> any_expr

let create_expr op a b =
  match op, a, b with
  | '+', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyInt,  Add (a, b))
  | '-', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyInt,  Sub (a, b))
  | '*', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyInt,  Mul (a, b))
  | '/', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyInt,  Div (a, b))
  | '<', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyBool, Lt  (a, b))
  | '>', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyBool, Gt  (a, b))
  | '&', Any (TyBool, a), Any (TyBool, b) -> Any (TyBool, And (a, b))
  | '|', Any (TyBool, a), Any (TyBool, b) -> Any (TyBool, Or  (a, b))
  | _, _, _ -> assert false

let eval_any : any_expr -> [> `Int of int | `Bool of bool] = function
  | Any (TyInt, expr) -> `Int (eval expr)
  | Any (TyBool, expr) -> `Bool (eval expr)

Answer 1

As you've found, this approach doesn't type check. It also has a more fundamental problem: GADTs can be recursive, in which case it is flatly impossible to enumerate their cases.

Instead you can reify types as a GADT and pass them around. Here's a cut-down example:

type _ expr =
  | Num : int -> int expr
  | Add : int expr * int expr -> int expr
  | Lt  : int expr * int expr -> bool expr
  | And : bool expr * bool expr -> bool expr

type _ ty =
  | TyInt : int ty
  | TyBool : bool ty

let bin_op (type a) (type b) op (l : a expr) (r : a expr) (arg_ty : a ty) (ret_ty : b ty) : b expr =
  match op, arg_ty, ret_ty with
  | '+', TyInt, TyInt -> Add (l, r)
  | '<', TyInt, TyBool -> Lt (l, r)
  | '&', TyBool, TyBool -> And (l, r)
  | _, _, _ -> assert false

At some point you are going to want to have a value that can be 'any expression'. Introducing an existential wrapper allows this. Cheesy example: generating random expression trees:

type any_expr = Any : _ expr -> any_expr

let rec random_int_expr () =
  if Random.bool () then Num (Random.int max_int)
  else Add (random_int_expr (), random_int_expr ())

let rec random_bool_expr () =
  if Random.bool () then Lt (Num (Random.int max_int), Num (Random.int max_int))
  else And (random_bool_expr (), random_bool_expr ())

let random_expr () =
  if Random.bool () then Any (random_int_expr ())
  else Any (random_bool_expr ())