types - OCaml:类型构造函数逃逸其范围的问题

Question

这是代码:

module type S = sig
  type t
  val do_it: t -> int -> t
end

let rec foo (type a) (module Foo:S with type t=a) (i:int) (x:a) = 
  if i=0 then x
  else foo (i-1) (Foo.do_it x i)

我收到此类型错误(在第 8 行，字符 17-32):

Error: This expression has type a but an expression was expected of type 'a
       The type constructor a would escape its scope

这是意外的，因为类型构造函数 a 仍在其范围内。我希望函数 foo 具有以下类型:

foo: (module S with type t = 'a) -> int -> 'a -> 'a

出了什么问题？

Answer 1

问题是多态递归:如果没有显式注释，函数 foo 的主体不能是多态的。写的时候

let rec foo (type a) (module Foo:S with type t=a) (i:int) (x:a) = 
  if i=0 then x
  else foo (module Foo:S with type t = a) (i-1) (Foo.do_it x i)

由于函数 foo 在其定义中不是多态的，因此它无法重用在其自身定义后引入的本地抽象类型 type a。

规避这个问题的一种方法是在本地抽象类型之后引入递归函数:

let foo (type a) =
  let rec foo (module Foo:S with type t=a) (i:int) (x:a) = 
  if i=0 then x
  else foo (module Foo) (i-1) (Foo.do_it x i) in
  foo

更经典的解决方案是为局部抽象类型添加显式通用量化a:

let rec foo: type a. (module S with type t=a) -> int -> a -> a =
fun (module Foo) i x ->
  if i=0 then x
  else foo (module Foo) (i-1) (Foo.do_it x i)