所以，这里涉及到两个概念：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 的范围。希望这会有所帮助:)