OCaml 类型系统的精妙之处：多态性、无点反向和嵌套列表

Posted 2023-02-19

【中文标题】OCaml 类型系统的精妙之处：多态性、无点反向和嵌套列表

【英文标题】：OCaml type-system subtlety: polymorphism, pointfree reverse, and nested lists

【发布时间】：2017-07-28 06:42:25

【问题描述】：

如果我这样定义一个反向函数：

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

让事情顺利进行。

这是怎么回事？

【参考方案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的形式，不受值限制。

一切都由此而来。

值限制在 Stack Overflow 上已经讨论过很多次了。这是一个这样的讨论：The value restriction。简短的总结是，在存在可变值（例如引用）的情况下，需要对使类型多态的某种限制。值限制是一种易于记住且不会过于限制的折衷方案。

当我开始忘记价值限制是什么时（定期发生），我经常参考这篇论文：Jacques Garrigue, Relaxing the Value Restriction