使用OCaml中的"constraint"关键字可以做些什么

Question

OCaml手册描述了"约束"关键字,该关键字可用于类型定义.但是,我无法弄清楚使用此关键字可以实现的任何用法.这个关键字什么时候有用？它可以用于删除多态类型变量吗？(这样一个模型中的'at变为t,模块可以用在一个functor参数中,它需要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; }

观察类型统一如何简化方程,在第一个例子中通过去除无关类型product(* 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