OCaml - GADT - bool 表达式

Question

我想知道是否有某种方法可以做到这一点:

type binary_operator = And | Or;;

type canonical;;
type not_canonical;;

type 'canonical boolean_expression =
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOp : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOp : _ boolean_expression * binary_operator * _ boolean_expression -> not_canonical boolean_expression
;;

这里的问题是我不能定义 BinOp 两次，而我想根据参数的类型...

PS:“规范”的意思是“表达式中包含的 n 个变量由 0 到 (n-1) 范围内的整数表示”。这是我需要对我的某些功能强制执行的不变量。

Answer 1

您必须为类型构造函数指定不同的名称，因为在某些情况下 gadt 的行为确实类似于 adt。

让我们假设你想定义你的类型如下:

type 'canonical boolean_expression =
  | Bool : bool -> canonical boolean_expression (* here I assume that you wanted to have that case too *)
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOpNC : _ boolean_expression * binary_operator * _ boolean_expression -> not_canonical boolean_expression
 ;;

现在考虑稍加修改的类型:

type 'canonical boolean_expression =
  | Bool : bool -> canonical boolean_expression
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOpNC : 'a boolean_expression * binary_operator * 'a boolean_expression -> 'a boolean_expression
;;

现在，你可以得到 canonical boolean_expression 的二元运算。使用最后两个构造函数中的任何一个。
显然，通过任意选择结果值的类型而获得的自由有其后果:您可以创建具有重叠“类型案例”的小工具。这样做时，任何采用这些值之一的函数都必须测试这两种情况。因此构造函数的名称不能相同，因为类型可能不足以知道我们正在处理哪些值。

例如，下面的函数:

 let rec compute = function 
    | Bool b -> b   
    | BinOpC (a,And,b) -> compute a && compute b
    | BinOpC (a,Or,b) -> compute a || compute b
 ;;

给定你的定义，应该没有问题地检查和处理规范表达式。通过我的修改，编译器会理所当然地提示 BinOpNC也可以包含 canonical表达。

这似乎是一个暴露 gadt 方面的愚蠢示例(而且确实如此)，因为我修改后的 bool 表达式定义显然是不正确的(从语义上讲)，但编译器并不关心类型的实际含义。

本质上，gadt 仍然是 adt，因为您可能仍然会发现必须依靠构造函数来选择正确的操作过程的情况。