为啥部分应用程序有值限制？

Posted 2023-02-19

【中文标题】为啥部分应用程序有值限制？

【英文标题】：Why does a partial application have value restriction?为什么部分应用程序有值限制？

【发布时间】：2014-12-04 09:54:29

【问题描述】：

我可以理解allowing mutable是值限制和弱多态的原因。基本上，函数内部的可变 ref 可能会改变所涉及的类型并影响函数的未来使用。所以在类型不匹配的情况下可能不会引入真正的多态性。

例如，

# 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>

请记住，缓存最初是'a option，但是一旦第一次调用let () = remember 1，缓存就会变成int option，因此类型变得有限。值限制解决了这个潜在的问题。

---

我仍然不明白的是部分应用的价值限制。

例如，

let identity x = x
val identity: 'a -> 'a = <fun>

let map_rep = List.map identity
val map_rep: '_a list -> '_a list = <fun>

在上面的函数中，我没有看到任何 ref 或可变的地方，为什么仍然应用值限制？

【参考方案1】：

这是一篇很好的论文，描述了 OCaml 当前对值限制的处理：

Garrigue, Relaxing the Value Restriction

它对问题及其历史进行了很好的总结。

以下是一些观察结果，它们的价值。我不是专家，只是业余观察者：

术语“值限制”中的“值”含义是高度技术性的，与特定语言所操纵的值没有直接关系。这是一个句法术语；即，您可以通过查看程序的符号来识别值，而无需了解类型。

生成值限制过于严格的示例并不难。即，当值限制禁止时，泛化类型是安全的。但是试图做得更好（允许更多的概括）导致规则对于普通人（比如我自己）来说太难记住和遵循了。

准确概括何时安全的障碍不是单独编译 (IMHO)，而是停止问题。即，即使您看到所有程序文本，理论上也不可能。

【参考方案2】：

值限制非常简单：只有在语法上是值的 let-bound 表达式才会被泛化。应用程序，包括部分应用程序，不是值，因此不能泛化。

请注意，通常无法判断应用程序是否是部分的，因此无法判断应用程序是否会对参考单元格的值产生影响。当然，在这种特殊情况下，显然不会发生这样的事情，但推理规则的设计是为了在它发生的情况下是合理的。

【讨论】：

好的，我认为当编译器看到 ref 或检测到任何可变的时应用值限制。您能否在我的第一个 remember 示例中告诉我，这是一个让绑定，不是吗？另外，为什么编译器没有以检测ref 或可变然后应用值限制的方式构建？

好吧，被 let-bound 不足以成为多态。它还必须是“句法值”。至于第二个，我想关注的是单独编译。如果必须传递 Foo.f 是否涉及操纵引用的知识，以编译使用 Foo.f 的源代码，这将严重破坏单独编译。

第二个，在你的例子中Foo.f，如果Foo.f有一个ref，那么Foo.f的值已经限制了，对于其他涉及Foo.f的编译自然知道它来自它的签名，不是吗？

但无论如何，您能否像我在remember 示例中所做的那样，给我一个部分应用的示例？

Jackson，seanmcl链接的论文中给出了一个例子：搜索evil_map。

【参考方案3】：

“let”表达式不是（句法）值。虽然有一个“值”的precise definition，但大致上唯一的值是应用于值的标识符、函数、常量和构造函数。

This paper 及其引用的内容详细解释了该问题。

【讨论】：

但是remember函数是一个值吗？

let 表达式“评估”为一个值，该值是一个类型为 '_a -> '_a 的函数。结果值绑定到标识符“remember”。此后，remember 是一个值，因为它是一个句法标识符，因此是一个值。

您能否像我在remember 示例中所做的那样，给我一个部分应用的示例？

【参考方案4】：

部分应用不排除突变。例如，这是您的代码的重构版本，如果没有值限制，它也会不正确：

let aux cache x =
    match !cache with
    | Some y -> y
    | None -> cache := Some x; x

let remember = aux (ref None)