为什么“id id”不是 OCaml 中的值？

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

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

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

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

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

非正式地，语法值是一种无需进行任何计算即可计算的表达式，例如，考虑以下 let 绑定：

let f = g x 

这里不是语法值，因为为了获得值，您需要计算表达式。但是，在下文中，fg x

let f x = g x

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

let f = fun x -> g x

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

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

• 常量（即整数和浮点文字等）
• 仅包含其他简单值的构造函数
• 函数声明，即以 fun 或 function 开头的表达式，或等效的 let 绑定，let f x = ...
• LET 形式的绑定 LET VAR = EXPR1 在 EXPR2 中，其中 EXPR1 和 EXPR2 都是简单值

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

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

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

let f = id id

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

现在，让我们来看看你的示例：

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

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

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

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