为什么'id id`不是OCaml中的值？

Question

我仍在尝试了解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似乎被视为值。

它们都是功能应用，有什么区别？

Answer 1

因此，这里涉及两个概念：let-polymoprhism和价值限制。让 - 多态性不允许所有非限制值的类型泛化。或者，在不使用双重否定的情况下，只有在引入了let-binding的情况下，才允许值为多态。这是一种过度逼近，即它可能不允许有效的程序（有误报），但它永远不会允许一个无效的程序（它将保持健全性）。

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

不过，让我先解释一下什么是语法值：

通俗地说，句法值是可以不用做任何的计算来计算的表达式，例如，请考虑下面就让结合：

let f = g x 

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

let f x = g x 

值f是语法，它会更明显，如果我们将删除糖：

let f = fun x -> g x 

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

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

• 常数（即，像整数和浮点文本）
• 构造函数，只有包含其他简单的值
• 函数声明，即表达式乐趣或功能，或等效让结合开始，let f x = ...
• 形式的let绑定让VAR =表达式1在表达式2，其中两个表达式1和表达式2是简单值

现在，当我们非常确定什么是语法的时候，让我们更仔细地看看你的例子。让我们从赖特的例子开始，实际上是：

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

，或者通过引入let id = fun x -> x

let f = id id 

您可能会看到，那f这里不是语法值，虽然id是语法。但为了得到f的值，你需要计算 - 所以这个值是在运行时定义的，而不是在编译时。

现在，让我们desugar你的例子：

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表达式。拉姆达表达式的类型是'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的范围。希望，这有助于:)

Answer 2

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

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