ocaml - OCaml 中的“约束”关键字可以做什么

Question

OCaml 手册描述了可以在类型定义中使用的“约束”关键字。但是，我无法弄清楚可以使用此关键字完成的任何用法。这个关键字什么时候有用？可以用来去除多态类型变量吗？（因此type 'a t模块中的 a 变得公正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