2

我仍在尝试了解 OCaml 中的值限制，并且正在阅读Wright 的论文。并且在其中声明(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似乎被视为一个值。

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

4

2 回答 2

3

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

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

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

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

let f = g x

这里f不是一个语法值，因为为了得到你需要计算的值 expression 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 的范围。希望，这会有所帮助:)

于 2017-02-10T14:23:24.980 回答
2

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

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

于 2017-02-10T00:37:15.383 回答