为什么在使用类类型时OCAML对象中的未绑定类型变量不会出现？

Question

我想了解OCAML对象的这种行为的原因.假设我有一个类A调用另一个类的对象的方法B.示意性地,A#f调用B#g和B#h.OOP中的常规做法是我希望避免将B用作固定的具体类,而是仅为B声明一个接口.在OCAML中执行此操作的最佳方法是什么？我尝试了几个选项,我不太明白为什么有些选项有效,有些则没有.这是代码示例.

版本1:

 # class classA = object
    method f b = b#g + b#h 
   end ;;
 Error: Some type variables are unbound in this type:
     class a : object method f : < g : int; h : int; .. > -> int end
   The method f has type (< g : int; h : int; .. > as 'a) -> int where 'a
   is unbound

这种行为是众所周知的:OCAML正确地推断出b具有开放对象类型<g:int;h:int;..>但后来抱怨我的类没有声明任何类型变量.如此看来,classA是需要有类型变量; 然后我明确地介绍了一个类型变量.

版本2:

 # class ['a] classA2 = object
   method f (b:'a) = b#g + b#h
   end ;;
 class ['a] classA2 :
   object constraint 'a = < g : int; h : int; .. > method f : 'a -> int end

这是有效的,但是现在这个类显然是多态的,带有类型约束,如OCAML所示.同样令人困惑的是类类型包含一个类型变量'a,但我仍然可以说let x = new classA2没有指定类型值'a.为什么会这样？

另一个缺点classA2是显式类型约束(b:'a)包含类型变量.毕竟,我知道b必须符合固定的界面而不是未知的类型'a.我希望OCAML验证此接口确实是正确的.

所以在版本3中,我首先将接口声明classB为类类型,然后声明b必须是这种类型:

 # class type classB = object method g:int method h:int end;;
 class type classB = object method g : int method h : int end
 # class classA3 = object method f (b:classB) = b#g + b#h end;;
 class classA3 : object method f : classB -> int end

这也有效,但我的困惑仍然存在:为什么不再classA3需要显式多态性？

问题摘要:

• 为什么可以在new classA2不指定类型的情况下使用,'a即使classA2使用类型变量声明'a？
• 为什么classA3接受类型约束(b:classB)并且不再需要绑定类型变量？
• 以某种微妙的方式是功能classA2和classA3不同,如果是,如何？

Answer 1

这有点复杂,所以要紧紧抓住.首先,让我添加一个classA4变体,这恰好是你真正需要的.

class classA4 = object
  method f : 'a. (#classB as 'a) -> int = fun b -> b#g + b#h
end

类classA2,classA3并且classA4都是微妙的不同,不同之处在于OCaml如何处理类型多态和对象多态.让我们假设两个类,b1并b2实现classB类型.

就对象多态性而言,这意味着b1可以classB使用强制语法将类型的表达式强制转换为类型(new b1 :> classB).此类型强制丢弃类型信息(您不再知道对象是类型b1),因此必须使其显式化.

就类型多态性而言,这意味着b1可以使用类型代替具有约束#classB(或< g : int ; h : int ; .. >)的任何类型变量.这不会丢弃任何类型信息(因为类型变量被实际类型替换),因此它由类型推断算法执行.

方法f的classA3期望类型的参数classB,这意味着一个类型强制是强制性的:

let b = new b1 
let a = new classA3
a # f b (* Type error, expected classB, found b1 *)
a # f (b :> classB) (* Ok ! *)

这也意味着(只要您强制执行),classB可以使用任何实现类.

法f的classA2要求类型匹配约束的参数#classB,但OCaml的任务,这样的类型不应该是未绑定,所以它在类级别的约束.这意味着每个实例都classA2将接受实现的单个任意类型的参数classB(并且该类型将是类型推断的).

let b1 = new b1 and b2 = new b2
let a  = new classA2 
a # f b1 (* 'a' is type-inferred to be 'b1 classA2' *)
a # f b2 (* Type error, because b1 != b2  *)

重要的是要注意classA3相当于classB classA2,这就是为什么它不需要绑定类型变量,以及为什么它严格地表达不如classA2.

方法f的classA4已经给出使用明确的类型'a.语法,这在方法级别而不是类级别结合型变量.它实际上是一个通用的量词,这意味着«可以为任何'a实现的类型调用此方法#classB»:

let b1 = new b1 and b2 = new b2
let a  = new classA4
a # f b1 (* 'a is chosen to be b1 for this call *)
a # f b2 (* 'a is chosen to be b2 for this call *)