价值约束

Question

在OCaml中，你不能泛化部分应用的柯里化函数（“值约束”）。

值约束的目的是什么？如果它不存在会出现什么不好的情况？

- ThePiercingPrince

Answer 1

如果没有价值限制或其他限制泛化的机制，这个程序将被类型系统接受：

let r = (fun x -> ref x) [];; (* this is the line where the value restriction would trigger *)

> r : 'a list ref

r := [ 1 ];;

let cond = (!r = [ "foo" ]);;

变量r的类型应为'a list ref，这意味着它的内容可以与[ "foo" ]进行比较，即使它包含一个整数列表。

请参阅Xavier Leroy的博士论文获取更多动机（ref并不是唯一可能添加到纯λ演算中引入问题的构造），以及他的论文所提到的系统的概述（包括他的系统）。

- Pascal Cuoq

---

@ThePiercingPrince 现代 OCaml 中使用的解决方案令人不快的地方在于，如果你编写纯函数式的 OCaml 代码，即使不必要（因为你的程序是通过纯函数实现安全的），值限制仍然适用于你。X.L.论文中描述的某些系统没有这个缺点，但它们会揭示类型的实现细节。由于模块化被认为是下一个重要的事情，选择了简化模块化的解决方案。旧版本的 Caml-light 已经实现了 X.L.论文中的系统... - Pascal Cuoq

这是最复杂的之一（我非常确定），允许编写所有纯函数Caml程序。虽然你必须回到旧的Caml-light版本。正如你所说，如果想编写纯函数式程序，请使用Haskell。下一个Haskell版本将会是严格模式。 - Pascal Cuoq

@ThePiercingPrince 在 http://www.cs.nott.ac.uk/~gmh/appsem-slides/peytonjones.ppt 中查找：下一个 Haskell 将是严格的，下一个 ML 将是纯的。 - Pascal Cuoq

@ThePiercingPrince，不要太高兴 ;)。首先，Haskell有单态化限制，与值限制几乎相同，但仅适用于存在类约束时。其次，更糟糕的是，unsafePerformIO实际上引入了ML中值限制旨在解决的问题。也就是说，使用unsafePerformIO，你可以在Haskell中编写一个不安全的通用转换函数，并让一切都失控。 - Andreas Rossberg

@AndreasRossberg，但作为权衡的正交轴，全局类型推断问题不是源自于哪里吗（https://github.com/keean/zenscript/issues/33#issuecomment-362533360），因此一个替代方案可以保留模块化并消除限制，就是注释闭包的所有自由变量的类型，似乎 Scala 就需要这样做？ - Shelby Moore III

Answer 2

这里是我之前关于F#的答案；用OCaml时也会遇到同样的问题。问题在于，如果没有它，我们就可能创建指向错误类型数据的引用：

let f : 'a -> 'a option =
    let r = ref None in
    fun x ->
        let old = !r in
        r := Some x;
        old

f 3           // r := Some 3; returns None : int option
f "t"         // r := Some "t"; returns Some 3 : string option!!!

- Tarmil

Answer 3

这里有一个对于弱多态性（weakly polymorphism）的很好描述，可以在此处查看(side-effects-and-weak-polymorphism)。

基本上，让我们看一下下面这个函数（它会缓存它所见到的第一个值）：

# let remember =
    let cache = ref None in
    (fun x ->
       match !cache with
       | Some y -> y
       | None -> cache := Some x; x)
  ;;
val remember : '_a -> '_a = <fun>

由于它涉及到命令式，因此应用了“值限制”。

---

然而，让我们假设没有“值限制”。

那么它的类型就变成了val remember : 'a -> 'a = <fun>。

---

现在如果我执行let () = remember 1，那么1将被记录在cache中，对吗？

如果我第二次调用，let x = 3 + remember 2，这应该可以工作，因为3是整数，remember返回与其参数相同的类型。我在这里给出2，因此remember也会返回整数（但值为1，因为我们已经记住了一次）。这应该通过类型检查。

---

如果我第三次调用let y = 3.0 + remember 2.0，会再次工作吗？

根据remember的类型和我第二次调用的原因，它也应该工作，因为我给remember提供了浮点数，它应该返回浮点数。

但由于第一次它已经存储了一个整数1，所以它将返回一个整数1。因此，类型检查将失败，对吗？

---

我们可以看到，如果没有值限制或弱多态性，并且允许可变性，整个类型检查都会有问题。在上面的愚蠢情况下，您需要不断手动检查或跟踪remember存储的初始类型。

- Jackson Tale