OCAML类型系统微妙:多态性，无点反向和嵌套列表

Question

如果我定义了反向函数（

）

let reverse =
  let rec helper out = function
    | [] -> out
    | a :: l -> helper (a :: out) l
  in helper []

然后reverse (List.map reverse xs)不输入检查，而错误

Error: This expression has type 'a list list
   but an expression was expected of type 'a list
   The type variable 'a occurs inside 'a list

但用明确的参数定义它

let reverse l =
  let rec helper out = function
    | [] -> out
    | a :: l -> helper (a :: out) l
  in helper [] l

使事情起作用。

这里是怎么回事？

Answer 1

您的原始定义：

# let reverse =
    let rec helper out = function
      | [] -> out
      | a :: l -> helper (a :: out) l
      in helper [];;
val reverse : '_a list -> '_a list = <fun>

受到半著名值限制的约束，因为它具有应用程序的形式（即helper []），而不是lambda。

第二个定义具有lambda的形式，该形式不受价值限制。

其他所有内容都遵循。

在堆栈溢出上已经讨论了多次值限制。这就是这样的讨论：价值限制。简短的摘要是，在存在可变值（例如参考值）的情况下，需要对制作类型多态的某种限制。价值限制是一种妥协，很容易记住而不会被限制。

当我开始忘记价值限制的全部内容时（这是定期发生的），我经常提到本文：雅克·加里格（Jacques Garrigue），放松价值限制