我想知道是否有有这样的一些方法:OCaml的 - GADT - 布尔表达式
这里的问题是,我不能定义BinOp两次,而我想这取决于参数类型。 PS:“canonical”的意思是“包含在表达式中的n个变量用范围从0到(n-1)的整数”表示。这是一个不变的,我需要强制我的一些职能。
我想知道是否有有这样的一些方法:OCaml的 - GADT - 布尔表达式
这里的问题是,我不能定义BinOp两次,而我想这取决于参数类型。 PS:“canonical”的意思是“包含在表达式中的n个变量用范围从0到(n-1)的整数”表示。这是一个不变的,我需要强制我的一些职能。
你必须给出类型constuctors不同的名称,因为有些情况下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
使用最后两个构造函数中的任何一个。显然,通过任意选择结果值的类型而获得的自由具有其后果:您可以创建具有重叠“类型案例”的gad具。这样做时,任何采用这些值的函数都必须测试这两种情况。因此,构造函数的名称不能相同,因为类型可能不足以知道我们正在处理的值。
例如,下面的功能:
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仍然是adt,因为你仍然可以发现情况是你必须依靠构造函数来选择正确的行为。
你必须给他们具体的名字。否则,你将如何在你的代码中区分它们? – didierc
通过参数...两个'canonical boolean_expression'意味着它是第一个,其他意味着它是第二个。 – xavierm02