嵌套上下文中的显式多态注释

Question

在下面的代码中，我不确定我是否理解为什么_nested2.

这是否意味着只有顶级定义才能概括其推断类型以匹配显式多态签名？

let toplevel1 : 'a. 'a -> int = (fun _ -> 0)
let toplevel2 : 'a. 'a -> int = (fun (_ : 'a) -> 0)

let nest1 =
  let _nested1 : 'a. 'a -> int = (fun _ -> 0) in 0

let nest2 =
  let _nested2 : 'a. 'a -> int = (fun (_ : 'a) -> 0) in 0
(*                               ^^^^^^^^^^^^^^^^^^^
   Error: This definition has type 'a -> int which is less general than
            'a0. 'a0 -> int
*)

Answer 1

问题是注释'a中的类型变量(l': 'a t)存在于整个顶级定义中，因此比多态注释的寿命更长。

为了说明类型变量的作用域问题，请考虑

let int, id = 
  let f (x:'a) = x in
   (0:'a), f

在这里，也许令人惊讶的是， 的类型id最终是int ->int而不是'a. 'a -> 'a因为类型变量在和'a之间共享。(x:'a)(0:'a)

回到最后的问题，这意味着由于转义变量 ，尚无法概括函数_nested2第二行的类型。nest2'a

此外，只有最新版本的 OCaml（OCaml 4.11.0 之后）才具有该toplevel2功能：

let toplevel2 : 'a. 'a -> int = (fun (_ : 'a) -> 0)

被接受。

旧版本的 OCaml 失败并显示

错误：此定义的类型为“a -> int”，其通用性不如“a0”。'a0 -> 整数

因为早期版本中检查显式多态注释的算法没有检测到统一类型变量没有逃逸顶级定义的范围。

因此，简短的版本是最好不要将显式多态注释与（统一）类型变量混合。