5

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

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：“canonical”的意思是“表达式中包含的n个变量用0到(n-1)的整数表示”。这是一个不变量，我需要对我的某些功能强制执行。

4

1 回答 1

8

您必须为类型构造函数指定不同的名称，因为在某些情况下，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 的这一方面的一个愚蠢的例子（确实是这样），因为我对布尔表达式的修改定义显然是不正确的（从语义上讲），但编译器并不关心类型的语用含义。

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

于 2012-12-30T09:53:18.873 回答