在OCaml中创建GADT表达式 [英] Creating GADT expression in OCaml

问题描述

我的玩具GADT表情是:

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

评估功能:

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时，创建表达式很简单:

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

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

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

我的尝试:

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.

错误:此表达式的类型为int expr 但是期望使用a expr类型的表达式 int类型与a

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，我能够实现类型安全的评估程序.这里有两个技巧很重要:

UPDATE

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

• 现有包装器Any
• 类型标记(TyInt和TyBool)，使我们可以对Any类型进行模式匹配

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

请参见

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)

推荐答案

如您所见，这种方法不会键入check.它还存在一个更基本的问题:GADT可以递归，在这种情况下，几乎不可能枚举其案例.

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.

相反，您可以将类型验证为GADT并将其传递给周围.这是一个简化的示例:

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

这篇关于在OCaml中创建GADT表达式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！