为什么`id id`不是OCaml中的值？ [英] Why `id id` is not a value in OCaml?
问题描述
我仍试图理解OCaml中的价值限制，并通过阅读赖特的论文。并且在其中声明（fun x - > x）（fun y - > y）不是一个语法值，同时它也表示lambda表达式应该是一个值。我在这里有点困惑，它不是 id id ，它本质上也是一个lambda表达式？真正算作OCaml语法值的是什么？
我也在 utop 中试过它，发现这些： y）（fun z - > z）
val x：'_a - > '_a =< fun>
这里 id id 不是一个值，它不能逃避价值限制，但是
utop＃let xa = let x =（fun y - > y）a in x ;;
val x：'a - > 'a =< fun>
这里 id a 似乎被视为一个值。
它们都是功能应用程序，有什么区别？因此，这里涉及两个概念：let-polymoprhism和价值限制。让 - 多态性不允许所有非限制值的类型泛化。或者，在不使用双重否定的情况下，只有在引入了let-binding的情况下，才允许值为多态。这是一种过度逼近，即它可能不允许有效的程序（有误报），但它永远不会允许一个无效的程序（它将保持健全性）。
价值限制是另一种过度逼近，需要保持命令式程序的正确性。它不允许非语法值的多态。 OCaml使用这种过度逼近的更精确版本，称为放松值限制（实际上允许某些非语法值是多态的）。
但是，让我先解释一下什么是句法值：
非正式地，语法值是一个表达式可以在不做任何计算的情况下进行评估，例如，考虑下面的绑定：
let f = gx
code> 这里 f 不是一个语法值，因为为了获得值你需要计算表达式 gx 。但是，在下文中，
let fx = gx
值 f 是句法的，如果我们删除糖，它会更明显：
let f = fun x - > gx
现在很明显， f 是语法的，因为它绑定到lambda表达式。
该值被称为语法，因为它直接在程序中定义（在语法中）。基本上，它是一个可以在静态时间计算的常数值。稍微正式一些，下面的值被认为是语法的：
- 常量（即像整型和浮点型文字）
- 只包含其他简单值的构造函数
- 函数声明，即以fun或function开头的表达式或等效的let绑定
let fx = ... - 让expr2中let var = expr1形式的绑定，其中expr1和expr2都是简单值
现在，当我们非常确定什么是语法的时候，让我们更仔细地看看您的示例。实际上，我们从Wright的例子开始：
let f =（fun x => x）（fun y =>> y）
或者，通过介绍 let id = fun x - > x
let f = id id
您可能会发现，这里 f 不是一个语法值，尽管 id 是句法。但是为了得到 f 的值，你需要计算 - 所以这个值是在运行时定义的，而不是在编译时。
现在，让我们来看看你的例子：
let xa = let x =（fun y - > y）a in x
==>
let x = fun a - >让x =（fun y - > y）a in x
我们可以看到， x 是一个语法值，因为左边是一个lambda表达式。 lambda表达式的类型是'a - > 一。你可能会问，为什么表达式的类型不是'_ a - > _a 。这是因为值限制只在顶层引入，并且lambda表达式还不是一个值，它是一个表达式。从外行的角度来说，首先，最普遍的Hindley-Milner类型是根据假设推断的，即没有副作用，然后通过（放松）价值限制来减弱推断类型。类型推断的范围是一个 let 绑定。
这是所有的理论，有时它并不是很明显为什么有些表达式是正确类型的，而具有相同语义但写法略有不同的表达式没有很好的类型。直觉可能会说，这里有什么问题。事实上，它实际上是 let f = id id 是一个格式良好的程序，被类型检查程序拒绝，这是 - 近似。如果我们将这个程序转换为 let fx = id id x ，它会突然变成一个具有一般类型的良好类型的程序，尽管转换不会改变语义（和这两个程序实际上编译成相同的机器码）。这是一个类型系统的局限性，它是简单性和精确性之间的妥协（稳健性不能成为妥协的一部分 - 类型检测器必须是合理的）。所以，从理论上来说，后一个例子总是安全的，这完全不明显。为了实验的目的，我们试着玩玩你的例子，并尝试打破这个程序：
＃let x = fun a - >让z = ref无x =（fun y - > z：= Some y; y）a in x ;;
val x：'a - > 'a =< fun>
因此，我们在这里添加了一个引用 z ，并且我们试图存储这个值，以便在不同类型的应用程序下，我们应该能够存储不同类型的相同参考值。然而，它是完全不可能的，因为因为 x 是一个语法值，所以保证每一个类型 xk 被称为一个新的引用被创建，并且这个引用永远不会泄漏let-definition的范围。希望，这有助于：）
I am still trying to understand the value restriction in OCaml and I was reading through Wright's paper. And in it states (fun x -> x) (fun y -> y) is not a syntactic value while it is also stating lambda expression should be a value. I am a bit confused here, isn't id id in its essence also a lambda expression? What really counts as a syntactic value in OCaml?
I also tried it in utop and found these:
utop # let x = let x = (fun y -> y) (fun z -> z) in x ;;
val x : '_a -> '_a = <fun>
Here id id is not a value and it cannot escape the value restriction but
utop # let x a = let x = (fun y -> y) a in x ;;
val x : 'a -> 'a = <fun>
Here id a seems to be treated as a value.
They are all function application, what's the difference?
So, there are two concepts involved here: let-polymoprhism and value restriction. Let-polymorphism disallows type generalization for all values that are not let-bound. Or, without using a double negation, it allows a value to be polymorphic only if it is introduced with the let-binding. This is an over-approximation, i.e., it may disallow valid programs (there are false positive), but it will never allow an invalid program (it will preserve the soundness).
The value restriction is another over-approximation, that is needed to preserve the soundness of imperative programs. It disallows polymorphism for non-syntactic values. OCaml uses a more precise version of this over-approximation that is called a relaxed value restriction (that actually allows certain non-syntactic values to be polymorphic).
But let me first explain what is a syntactic value:
Informally, a syntactic value is an expression that can be evaluated without doing any computation, e.g., consider the following let binding:
let f = g x
Here f is not a syntactic value because in order to get the value you need to compute expression g x. But, in the following,
let f x = g x
the value f is syntactic, it would be more obvious, if we will remove the sugar:
let f = fun x -> g x
Now it is obvious, that f is syntactic as it is bound to a lambda-expression.
The value is called syntactic because it is defined directly in the program (in the syntax). Basically, it is a constant value that can be computed at static time. Slightly more formally, the following values are considered syntactic:
- Constants (i.e., things like integer and floating-point literals)
- Constructors that only contain other simple values
- Function declarations, i.e., expressions that begin with fun or function, or the equivalent let binding,
let f x = ... - let bindings of the form let var = expr1 in expr2, where both expr1 and expr2 are simple values
Now, when we're pretty sure what is syntactic what is not, let's look at your examples more closely. Let's start with the Wright's example, actually:
let f = (fun x => x) (fun y => y)
or, by introducing let id = fun x -> x
let f = id id
You may see, that f here is not a syntactic value, although id is syntactic. But in order to get the value of f you need to compute - so the value is defined at runtime, not in the compile time.
Now, let's desugar your example:
let x a = let x = (fun y -> y) a in x
==>
let x = fun a -> let x = (fun y -> y) a in x
We can see, that x is a syntactic value, because to the left is a lambda expression. The type of lambda expression is 'a -> 'a. You may ask, why the type of the expression is not '_a -> '_a. This is because the value restriction is introduced only on the top-level, and lambda expression is not a value yet, it is an expression. In layman terms, first, the most general Hindley-Milner type is inferred under an assumption, that there are no side effects, and then the inferred type is weakened by the (relaxed) value restriction. The scope of type inference is a let binding.
This is all theory, and sometimes it is not really obvious why some expressions are well-type, while expressions with the same semantics, but written slightly different, are not well typed. The intuition might say, that there is something wrong here. And yes it is, in fact, let f = id id is a well-formed program that is declined by a typechecker, and this is an example of the over-approximation. And if we will transform this program to let f x = id id x it suddenly becomes a well typed program with a general type, although the transformation doesn't change the semantics (and both programs are actually compiled to the same machine code). This is a limitation of a type system, that came as a compromise between simplicity and precision (the soundness can't be a part of compromise - typechecker must be sound). So, it is totally not obvious from the theory why the latter example, is always safe. Just for the sake of experiment let's try to play with your example, and try to break the program:
# 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>
So, we added a reference z here, and we're trying to store the value, so that under different applications to different types, we should be able to store to the same reference values of different types. However, it is totally non-possible, since because x is a syntactic value, it is guaranteed, that every type x k is called an new reference is created, and this reference will never leak the scope of let-definition. Hope, that this helps :)
这篇关于为什么`id id`不是OCaml中的值？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
