OCaml中如何对lambda参数全称量化实现类似Rank2Types的多态效果

问题本质 #

你编写的代码中，类型变量'a默认在foo函数的最外层做全称量化，对应类型为forall 'a. ('a -> unit) -> unit。这个类型的语义是：调用foo时由调用方选定'a的具体类型，一旦选定全程固定。第一次调用f 1会把'a推导为int，后续传入字符串参数自然会触发类型不匹配错误。

你需要的是Rank-2多态效果：参数f本身是独立的多态函数，类型为(forall 'a. 'a -> unit) -> unit，f的多态性由foo的实现方持有，在foo内部可以多次将f实例化为不同参数类型调用，和开启Rank2Types扩展的Haskell逻辑完全一致。

实现方案 #

OCaml原生支持Rank-N多态，只需要显式标注全称量词，并且将多态参数存放在支持承载多态值的结构中即可，最简洁、兼容性最好的写法是使用单字段记录（OCaml的记录字段天然支持存放任意rank的多态值）：

(* 与Haskell Rank2Types实现语义完全等价 *)
let foo { f : 'a. 'a -> unit } =
  f 1;
  f "s"

代码中'a. 'a -> unit就是对字段f的显式全称量化，表示f是一个可适配任意输入类型的多态函数。

调用示例 #

(* 传入多态函数测试，可正常编译运行 *)
let () =
  foo {
    f = fun _ -> print_endline "received value"
  }

补充说明 #

OCaml 4.13及以上版本也支持直接在函数参数位置写显式多态标注，写法更简洁，但对旧版本编译器兼容性不如单字段记录方案：

let foo (f : 'a. 'a -> unit) =
  f 1;
  f "s"

更高阶的Rank-N多态场景也可以沿用同样思路，把需要独立多态性的部分放在记录字段中，显式标注对应位置的全称量词即可，不需要额外开启语言扩展。

内容的提问来源于stack exchange，提问作者namesis