在 OCaml 中创建 GADT 表达式

Question

有我的玩具GADT表情：

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

评价函数：

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)

当我们限制为 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

问题是如何在 create_expr 函数中同时支持 int expr 和 bool expr。

我的尝试：

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

它仍然不能return泛化类型的值。

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

更新

感谢@gsg，我能够实现类型安全的求值器。有两个技巧很重要：

存在包装器Any
类型标记（TyInt 和 TyBool）让我们可以模式匹配 Any 类型

见

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

您为 create_expr 指定的类型是 char -> 'a expr -> 'a expr -> 'a expr。但是 '>' 案例的类型将是 char -> int expr -> int expr -> bool expr。看来基本方案有问题。

本质上，您希望结果的类型取决于字符的值。我不是绝对肯定，但我怀疑这在 OCaml 中是不可能的。似乎需要更强大的类型系统。

Answer 2

如您所见，此方法不进行类型检查。它还有一个更根本的问题：GADT 可以递归，在这种情况下，根本不可能枚举它们的情况。

相反，您可以将类型具体化为 GADT 并传递它们。这是一个缩减示例：

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

在某些时候，您会想要一个可以是 'any expression' 的值。引入存在性包装器允许这样做。俗气的例子：生成随机表达式树：

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 ())

在 OCaml 中创建 GADT 表达式

Creating GADT expression in OCaml

ocaml

gadt

更新