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)