2

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

我写道：

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 他们都是值得的。

4

3 回答 3

3

As I explained before, the need for the value restriction -- or something similar -- arises when you combine parametric polymorphism with mutable references (or certain other effects). That is completely independent from whether the language has type inference or not or whether the language also allows subtyping or not. A canonical counter example like

let r : ∀A.Ref(List(A)) = ref [] in
r := ["boo"];
head(!r) + 1

is not affected by the ability to elide the type annotation nor by the ability to add a bound to the quantified type.

Consequently, when you add references to F<: then you need to impose a value restriction to not lose soundness. Similarly, MLsub cannot get rid of the value restriction. Scala enforces a value restriction through its syntax already, since there is no way to even write the definition of a value that would have polymorphic type.

于 2018-02-03T16:15:17.140 回答
2

它比这简单得多。在 Scala中，值不能有多态类型，只有方法可以。例如，如果你写

val id = x => x

它的类型不是[A] A => A。

如果你采用多态方法，例如

 def id[A](x: A): A = x

并尝试将其分配给一个值

 val id1 = id

编译器将再次尝试（在这种情况下失败）推断特定A而不是创建多态值。

所以这个问题不成立。

编辑：

如果您尝试在 Scala 中重现http://mlton.org/ValueRestriction#_alternatives_to_the_value_restriction示例，您遇到的问题不是缺少let:val与它完全对应。但是你需要类似的东西

val f[A]: A => A = {
  var r: Option[A] = None
  { x => ... }
}

这是非法的。如果你写def f[A]: A => A = ...它是合法的，但r在每次调用时都会创建一个新的。在 ML 术语中，它就像

val f: unit -> ('a -> 'a) =
    fn () =>
       let
          val r: 'a option ref = ref NONE
       in
          fn x =>
          let
             val y = !r
             val () = r := SOME x
          in
             case y of
                NONE => x
              | SOME y => y
          end
       end

val _ = f () 13
val _ = f () "foo"

这是值限制所允许的。

也就是说，Scala 的规则相当于只允许 lambda 作为 ML 中的多态值，而不是所有值限制所允许的。

于 2018-02-03T08:40:56.450 回答
1

编辑：这个答案之前是不正确 的。我已经完全重写了下面的解释，以从 Andreas 和 Alexey 的答案下的评论中收集我的新理解。

这个页面在archive.is的编辑历史和档案历史记录了我之前的误解和讨论。我选择编辑而不是删除并编写新答案的另一个原因是保留对此答案的评论。IMO，仍然需要这个答案，因为尽管 Alexey 正确且最简洁地回答了主题标题——而且 Andreas 的阐述对我获得理解最有帮助——但我认为外行读者可能需要一个不同的、更全面的（但希望仍然生成本质）解释，以便快速获得对该问题的一些深入理解。此外，我认为其他答案掩盖了整体解释的复杂程度，我希望天真的读者可以选择品尝它。

值限制出现在我们对引用的1 类型参数化对象2进行突变的情况下。在以下MLton 代码示例中演示了在没有值限制的情况下会导致的类型不安全：

val r: 'a option ref = ref NONE
val r1: string option ref = r
val r2: int option ref = r
val () = r1 := SOME "foo"
val v: int = valOf (!r2)

引用的对象中包含的NONE值（类似于）可以分配给类型参数的任何具体类型的引用，因为它具有多态类型。这将允许类型不安全，因为如上面的示例所示，引用的同一对象已分配给两者，并且可以通过引用用值写入（即变异），然后通过引用作为值读取。对于上述示例，值限制会生成编译器错误。nullr'ara'rstring option refint option refstringr1intr2

出现类型复杂化以防止3所述引用（及其指向的对象）的类型参数（即类型变量）的（重新）量化（即绑定或确定）到在重用实例时不同的类型表示先前用不同类型量化的参考。

例如，在连续的函数应用程序（也称为调用）重用此类引用的相同实例的情况下，就会出现这种（可以说是令人困惑和令人费解的）情况。IOW，每次应用函数时（重新）量化引用的类型参数（与对象有关）的情况，但引用的相同实例（及其指向的对象）被重复用于每个后续应用程序（和量化）函数。

切线地，由于缺乏明确的全称量词∀（因为隐含的rank-1 前置词法范围量化可以通过诸如let或协程之类的结构从词法评估顺序中移出）和可以说更大的不规则性（与 Scala 相比）在 ML 的值限制中何时可能出现不安全情况：

安德烈亚斯写道：

不幸的是，ML 通常不会在其语法中明确量词，仅在其类型规则中。

例如let，类似于数学符号的表达式需要重用引用的对象，即使它们可能在子句中多次被词法替换，也应该只创建和评估一次替换的实例化。因此，例如，如果函数应用程序在子句中被评估为（无论是否也在词法上），而替换的类型参数为每个应用程序重新量化（因为替换的实例化仅在词法上inin在函数应用程序中），那么如果不是所有应用程序都被迫只量化一次有问题的类型参数（即不允许有问题的类型参数是多态的），则类型安全可能会丢失。

值限制是 ML 在防止所有不安全情况的同时也防止一些（以前认为是罕见的）安全情况的折衷方案，以简化类型系统。值限制被认为是更好的折衷方案，因为早期（过时？）使用更复杂的打字方法的经验没有限制任何或尽可能多的安全案例，导致命令式编程和纯函数式（又名应用程序）编程之间出现分歧，并泄露了一些ML函子模块中抽象类型的封装。我引用了一些资料并在这里进行了详细说明。不过，切切地，我正在思考早期的论点是否反对分岔确实反对这样一个事实，即按名称调用根本不需要值限制（例如，当也需要记忆时，Haskell-esque惰性求值），因为从概念上讲，部分应用程序不会在已经评估的状态上形成闭包；模块化组合推理需要按名称调用，当与纯度结合时，则需要模块化（范畴论和等式推理）控制和效果组合。反对按名称调用的单态化限制论点实际上是关于强制类型注释，但是在需要优化记忆（又名共享）时明确说明可以说是不那么繁重的，因为任何方式都需要所述注释以实现模块化和可读性。Call-by-value 是一种精细的梳状控制级别，因此在我们需要低级别控制的地方，也许我们应该接受值限制，因为更复杂的类型所允许的罕见情况在命令式与命令式相比不太有用应用设置。但是，我不知道这两者是否可以用相同的编程语言以平滑/优雅的方式分层/隔离。代数效应可以用 CBV 语言（如 ML）实现，它们可以避免值限制。IOW，如果值限制正在影响您的代码，可能是因为您的编程语言和库缺少合适的元模型来处理效果。

Scala对所有此类引用进行了语法限制，这是一种折衷方案，例如限制相同甚至更多的情况（如果不限制，那将是安全的），而不是 ML 的值限制，但在某种意义上更规则，我们不会对与值限制有关的错误消息摸不着头脑。在 Scala 中，我们从不允许创建这样的引用。因此，在 Scala 中，我们只能表达在量化类型参数时创建引用的新实例的情况。注意OCaml在某些情况下放宽了值限制。

注意 afaik Scala 和 ML 都不允许声明引用是不可变的1，尽管它们指向的对象可以声明为不可变的1 val。请注意，没有必要对不能变异的引用进行限制。

之所以需要引用类型1的可变性以产生复杂的类型案例，是因为如果我们let使用非参数化对象（即 notNone或Nil4 but而不是例如 aOption[String]或List[Int])，则参考将没有多态类型（与它指向的对象有关），因此永远不会出现重新量化问题。因此，有问题的情况是由于使用多态对象进行实例化，然后在重新量化的上下文中分配一个新量化的对象（即改变引用类型），然后在随后的引用中从（指向的对象）引用中解引用（读取）重新量化的上下文。如前所述，当重新量化的类型参数发生冲突时，就会出现类型复杂化，并且必须防止/限制不安全的情况。

呸！如果您在不查看链接示例的情况下理解这一点，我会印象深刻。

1 IMO 改为使用短语“可变引用”而不是“被引用对象的可变性”和“引用类型的可变性”会更容易混淆，因为我们的意图是改变对象的值（及其类型），即被指针引用——不是指引用指向的指针的可变性。一些编程语言甚至没有明确区分它们何时不允许在原始类型的情况下选择改变引用或它们指向的对象。

2 其中一个对象甚至可以是一个函数，在允许一流函数的编程语言中。

3 为了防止在运行时由于访问（读取或写入）引用的对象而出现分段错误，并假设其静态（即在编译时）确定的类型不是对象实际具有的类型。

4 分别在 ML中NONE。[]

于 2018-02-03T06:50:22.647 回答