多态递归上下文中的局部抽象类型 VS 显式多态性

Question

你能解释一下为什么这个程序要进行类型检查吗

let rec plop1 : 'a 'b 'c. 'a -> 'b * 'c = 
  fun x -> (fst (plop1 ""), snd (plop1 1))

而这个没有？

let rec plop2 (type a b c) (x : a) : b * c = 
  (fst (plop2 ""), snd (plop2 1))

我已经在 OCaml 手册中阅读了本地抽象类型的定义；

'a.

和

type a.

之间有什么区别以及何时使用？；和类型变量和局部抽象类型有什么区别？，但它们对我来说还不够清楚。

Answer 1

多态递归需要函数类型的显式多态注释。这是为了能够使用此显式类型作为其自身函数体内的函数的类型。例如，

type 'a btree = Leaf of 'a | Node of ('a * 'a) btree
let rec sum: 'a. ('a -> int) -> 'a btree -> int =
fun f btree -> match btree with
| Leaf x -> f x
| Node x -> sum (fun (x,y) -> f x + f y) x
let sum = sum Fun.id

请参阅 https://ocaml.org/manual/5.2/polymorphism.html#s%3Apolymorphic-recursion 了解更多详细信息。

在第二种情况下，整个函数没有这样的显式类型注释

let rec plop2 (type a b c) (x : a) : b * c = 
  (fst (plop2 ""), snd (plop2 1))

仅对函数的parts进行一些注释。这是一个有意义的差异，因为值通常仅在

let

上实现多态。

更一般地说，局部抽象类型与多态递归并不真正相关。局部抽象类型引入了新的类型名称，可以在类型定义中使用，或者在与 GADT 的模式匹配分支内添加局部方程。换句话说，

fun (type a) -> ...

相当于假设

let type a in ... (* <1> *)

创建了一个仅限于范围

<1>

范围内的新鲜抽象类型。

值得注意的是，这意味着 OCaml 结构

fun (type a) -> ...

不 等同于 system-F

𝛬

。 例如，

fun (type a) (x:a) -> ...

不等于

𝛬a. 𝜆(x:a) ...

。

OCaml 中更接近的转录可能是

let f: type a. a -> _ = ...

但是这个符号本身就是一个语法糖

let rec plop2: 'a. 'a -> _ = fun (type a) (x:a) ->
  fst (plop2 ""), snd (plop2 1)

这是对于多态递归很重要的第一部分。