ocaml - OCaml 中的 "constraint"关键字可以做什么

Question

The OCaml manual描述了可以在类型定义中使用的“约束”关键字。但是，我无法弄清楚可以使用此关键字完成的任何用法。这个关键字什么时候有用？可以用来去除多态类型变量吗？ (这样模块中的 type 'a t 就变成了 t，并且该模块可以在需要 t 且没有变量的仿函数参数中使用。)

Answer 1

所以，constraint关键字，在类型或类定义中使用，可以说让一个人将适用类型的范围“缩小”为类型参数。文档明确宣布，约束方程两边的类型表达式将统一“细化”约束相关的类型。因为它们是类型表达式，所以您可以使用所有常用的类型级别运算符。

例子:

# type 'a t = int * 'a constraint 'a * int = float * int;;
type 'a t = int * 'a constraint 'a = float

# type ('a,'b) t = 'c r constraint 'c = 'a * 'b
    and 'a r = {v1 : 'a; v2 : int };;
type ('a,'b) t = ('a * 'b) r
and 'a r = { v1 : 'a; v2 : int; }

观察类型统一如何简化方程，在第一个示例中通过去除无关的类型乘积 ( * int)，在第二个示例中完全消除它。另请注意，我使用了类型变量 'c它只出现在类型定义的右侧。

两个有趣的用途是多态变体和类类型，它们都基于行多态。约束允许表达某些子类型关系。通过子类型化，对于变体，我们指的是这样一种关系，即任何类型的构造函数都存在于其子类型中。其中一些关系可能已经单态地表示:

# type sum_op = [ `add | `subtract ];;
type sum_op = [ `add | `subtract ]
# type prod_op = [ `mul | `div ];;
type prod_op = [ `mul | `div ]
# type op = [ sum_op | prod_op ];;
type op = [ `add | `div | `mul | `sub ]

那里， op是 sum_op 的子类型和 prod_op .

但在某些情况下，您必须引入多态性，这就是约束派上用场的地方:

# type 'a t = 'a constraint [> op ] = 'a;;
type 'a t = 'a constraint 'a = [> op ]

以上让您表示类型族，它们是 op 的子类型。 : 类型实例为 'a本身对于 'a t 的给定实例.

如果我们尝试在没有参数的情况下定义相同的类型，类型统一算法会报错:

# type t' = [> op];;
Error: A type variable is unbound in this type declaration.
In type [> op ] as 'a the variable 'a is unbound

相同种类的约束可以用类类型表示，如果类型定义通过子类型隐式多态，则可能出现相同的问题。

# class type ct = object method v : int end;;
class type ct =  object method v : int end
# type i = #ct;;
Error: A type variable is unbound in this type declaration.
In type #ct as 'a the variable 'a is unbound
# type 'a i = 'a constraint 'a = #ct;;
type 'a i = 'a constraint 'a = #ct