为啥 `id id` 在 OCaml 中不是一个值？

Posted 2023-02-19

【中文标题】为啥 `id id` 在 OCaml 中不是一个值？

【英文标题】：Why `id id` is not a value in OCaml?为什么 `id id` 在 OCaml 中不是一个值？

【发布时间】：2017-06-28 05:16:25

【问题描述】：

我仍在尝试了解 OCaml 中的值限制，并且正在阅读 Wright's paper。并且在其中声明 (fun x -> x) (fun y -> y) 不是语法值，同时它还声明 lambda 表达式应该是一个值。我这里有点迷糊，id id 本质上不也是一个 lambda 表达式吗？在 OCaml 中什么才是真正的句法值？

我也在utop 中尝试过，发现了这些：

utop # let x = let x = (fun y -> y) (fun z -> z)  in x ;;
val x : '_a -> '_a = <fun>

这里id id不是一个值，也逃不过值的限制，但是

utop # let x a  = let x = (fun y -> y) a in x ;;
val x : 'a -> 'a = <fun>

这里id a 似乎被视为一个值。

都是函数式应用，有什么区别？

【问题讨论】：

OCaml 没有使用 Wright 论文中描述的值限制，而是使用更复杂的多级算法，其中句法值的概念被非扩展值的概念所取代，即没有可观察到的副作用的值。该算法更精确，类型更多的程序。因此，将 Wrights 论文直接应用于 OCaml 可能是个坏主意。非句法值可以在 OCaml 中泛化，因此并非所有具有通用类型的值都是句法值。我提供了一个详细的答案，我试图将重点放在句法值的一般概念上。

【参考方案1】：

所以，这里涉及到两个概念：let-polymorphism 和 value 限制。 Let-polymorphism 不允许对所有非 let-bound 的值进行类型泛化。或者，在不使用双重否定的情况下，它仅在使用 let 绑定引入时才允许值是多态的。这是一个过度近似，即它可能不允许有效程序（存在误报），但绝不会允许无效程序（它将保持健全性）。

值限制是另一种过度近似，需要保持命令式程序的健全性。它不允许非语法值的多态性。 OCaml 使用这种过度近似的更精确版本，称为relaxed value restriction（实际上允许某些 非语法值是多态的）。

但让我先解释一下什么是句法值：

非正式地，句法值是一个表达式，可以在不进行任何计算的情况下进行评估，例如，考虑以下 let 绑定：

let f = g x 

这里f 不是一个语法值，因为为了获得值，您需要计算表达式g x。但是，在下面，

let f x = g x

f 的值是语法，如果我们去掉糖会更明显：

let f = fun x -> g x

现在很明显，f 是语法，因为它绑定到 lambda 表达式。

该值被称为语法，因为它是直接在程序中定义的（在语法中）。基本上，它是一个可以在静态时间计算的常数值。稍微正式一点，以下值被视为语法：

常量（例如，整数和浮点字面量） 仅包含其他简单值的构造函数 函数声明，即以 fun 或 function 开头的表达式，或等效的 let 绑定 let f x = ... let 形式的绑定 let var = expr1 in expr2，其中 expr1 和 expr2 都是简单值

现在，当我们非常确定什么是句法什么不是时，让我们更仔细地看看你的例子。让我们从 Wright 的例子开始吧：

let f = (fun x => x) (fun y => y)

或者，通过介绍let id = fun x -> x

let f = id id

您可能会看到，f 这里不是句法值，尽管id 是句法值。但是为了获得 f 的值，您需要计算 - 所以该值是在运行时定义的，而不是在编译时定义的。

现在，让我们为您的示例脱糖：

let x a = let x = (fun y -> y) a in x
==>
let x = fun a -> let x = (fun y -> y) a in x 

我们可以看到，x 是一个语法值，因为左边是一个 lambda 表达式。 lambda 表达式的类型是'a -> 'a。你可能会问，为什么表达式的类型不是'_a -> '_a。这是因为值限制只在顶层引入，而 lambda 表达式还不是一个值，它是一个表达式。通俗地说，首先，最一般的 Hindley-Milner 类型是在没有副作用的假设下推断出来的，然后推断的类型被（松弛的）值限制削弱。类型推断的范围是 let 绑定。

这都是理论，有时并不是很明显为什么有些表达式是好类型的，而具有相同语义但写法略有不同的表达式却不是好类型。直觉可能会说，这里有问题。是的，事实上，let f = id id 是一个被类型检查器拒绝的格式良好的程序，这是 过度近似 的一个例子。如果我们将这个程序转换为let f x = id id x，它会突然变成一个具有通用类型的类型良好的程序，尽管转换不会改变语义（并且两个程序实际上都编译为相同的机器代码）。这是类型系统的限制，它是简单性和精确性之间的妥协（健全性不能成为妥协的一部分 - 类型检查器必须是健全的）。因此，从理论上完全不明显为什么后一个例子总是安全的。只是为了实验，让我们尝试使用您的示例，并尝试破坏程序：

# let x = fun a -> let z = ref None in let x = (fun y -> z := Some y; y) a in x ;;
val x : 'a -> 'a = <fun>

所以，我们在这里添加了一个引用z，并且我们正在尝试存储该值，这样在不同类型的不同应用下，我们应该能够存储不同类型的相同引用值。但是，这是完全不可能的，因为x 是一个语法值，所以可以保证，每个x k 被调用的类型都会创建一个新的引用，并且这个引用永远不会泄露let-definition 的范围。希望这会有所帮助:)

【参考方案2】：

这是一个应用程序，而不是 lambda 表达式。左边的表达式是一个函数，右边的表达式是一个应用函数的值。

值的概念（在值限制的意义上）是一个句法的概念。这与值的类型无关。

【讨论】：

utop # let x a = let x = (fun y -> y) a in x ;; val x : 'a -> 'a = <fun> 这里(fun y -> y) a 也是一个函数应用程序，但它通过了值限制。为什么？

它在语法上不是一个应用程序。从语法上讲，它是一个 lambda 表达式。 let x a = <expr> 是 let x = fun a -> <expr> 的精美语法。所以广义表达式的形式是fun a -> <expr>，一个lambda 表达式。 lambda 表达式中包含应用程序是可以的（自然）。