问题标签 [value-restriction]

根据标准 ML 的定义（修订版）：

这个想法是非扩展表达式的动态评估既不会产生异常也不会扩展内存的域，而扩展表达式的评估可能会。

[§4.7，第 19 页；强调我的]

我在网上找到了很多关于 ref-cell 部分的信息，但几乎没有关于异常部分的信息。（一些消息来源指出，多态绑定仍然有可能 raise Bind，并且这种不一致可能会产生类型理论和/或实现后果，但我不确定这是否相关。）

我已经能够提出一种与异常相关的不健全性，如果我没记错的话，它只能通过值限制来防止；但这种不健全并不取决于引发异常：

那么，谁能告诉我定义的含义，以及为什么它提到例外？

（“生成异常”是否可能意味着生成异常名称，而不是生成异常数据包？）

我在 OCaml 中编码一种 van Laarhoven 镜头，但由于价值限制而遇到困难。

相关代码如下：

在这里，我将镜头表示为更高阶的类型，即 CPS 转换函数的转换器（如此('a -> 'b) -> ('s -> 't)处所建议和所讨论的）。函数,和都具有完全泛化的类型，但它们的组合没有。lensfstbuildlens fst build

如要点所示，完全可以编写_1

但是每次都必须手动构建这些镜头很乏味，使用高阶函数（如lens.

有什么办法可以绕过这里的价值限制吗？

值限制错误：

无值限制错误：

为什么？

我正在构建一个合并排序函数，而我的拆分方法给了我一个值限制错误。我正在使用 2 个累积参数，即拆分产生的 2 个列表，最后我将它们打包成一个元组以供返回。但是我遇到了一个值限制错误，我无法弄清楚问题是什么。有没有人有任何想法？

任何输入表示赞赏。

我不明白该函数（my_path_mapper）不受值限制。

请教我为什么？

ML 中的值限制可防止在可能破坏类型安全的上下文中进行类型泛化。核心问题似乎来自于组合序列突变和多态类型，例如在这个 OCaml 代码中：

如果没有值限制，最后一行将进行类型检查而不会出错，因为多态类型 forx将与bool. 为了防止这种情况，for 的类型x必须保持单态。

我的问题如下：是否可以通过使用单子来表达操作序列来消除值限制？

作为函数参数，通过 monad 的bind操作引入的变量在整个序列中保持单态，因此在泛化过程中不引入特殊情况，似乎达到了与值限制相同的效果。

这行得通吗？如果不行，为什么？

给出一个值限制错误： error FS0030: Value restriction. The value 'empties' has been inferred to have generic type val empties : '_a list []. Either define 'empties' as a simple data term, make it a function with explicit arguments or, if you do not intend for it to be generic, add a type annotation.

虽然这不是：

那么区别是什么呢？我知道 SO 问题的传统包括“你尝试过什么”，但我什至不知道该尝试什么，这是一个概念性问题......

我仍在尝试了解 OCaml 中的值限制，并且正在阅读Wright 的论文。并且在其中声明(fun x -> x) (fun y -> y)不是语法值，同时还声明 lambda 表达式应该是一个值。我在这里有点困惑，id id本质上不也是一个lambda表达式吗？在 OCaml 中，什么才是真正的句法值？

我也试过了utop，发现了这些：

这里id id不是一个值，它不能逃脱值的限制，但是

这里id a似乎被视为一个值。

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

当参数为空列表时，List 模块中的某些函数会失败。List.rev 就是一个例子。问题是可怕的价值限制。

我在尝试定义一个返回列表的函数时遇到了同样的问题，该列表除了最后一个元素之外的所有元素：

该函数适用于非空列表，但处理空列表的版本失败：

我尝试了几件事：使其成为内联函数，不为参数指定类型，为返回值指定类型，使函数依赖于类型参数，并使用 Option 类型获取稍后转换为列表的中间结果<'一个>。没有任何效果。

例如，这个函数有同样的问题：

之前在 SO 中提出了一个类似的问题：空列表中的F# 值限制，但是当参数是空列表时，唯一的答案也会失败。

有没有办法编写一个同时处理空列表和非空列表的函数？

注意：该问题并非特定于返回列表中除最后一个元素之外的所有元素的函数。

这是我对这个问题的看法。任何人都可以确认、否认或详细说明吗？

我写道：

Scala 没有将协变与分配 给List[A]的 GLB ⊤统一起来，bcz afaics 在子类型化“biunification”</a> 中分配的方向很重要。因此必须有类型（即），同上类型不能分别接受来自or的赋值。因此，价值限制问题起源于无方向的统一，并且在最近的上述研究之前，全球双统一被认为是不可判定的。 List[Int]NoneOption[⊥]Option[Nothing]NilList[Nothing]Option[Int]List[Int]

您可能希望查看上述评论的上下文。

ML 的值限制将在（以前被认为是罕见但可能更普遍的）情况下不允许参数多态性，否则这样做是合理的（即类型安全），例如特别是对于 curried 函数的部分应用（这在函数式编程中很重要)，因为替代类型解决方案在函数式编程和命令式编程之间创建了分层，并打破了模块化抽象类型的封装。Haskell 有一个类似的双重单态限制。OCaml 在某些情况下放宽了限制。我详细阐述了其中一些细节。

编辑：我在上面引用中表达的原始直觉（子类型可以消除值限制）是不正确的。IMO 的答案很好地阐明了问题，我无法确定包含 Alexey、Andreas 或我的集合中的哪个应该是选定的最佳答案。IMO 他们都是值得的。