Scala 是否像 ML 一样有值限制,如果没有,那为什么?

Does Scala have a value restriction like ML, if not then why?

提问人:Shelby Moore III 提问时间:2/3/2018 最后编辑:Shelby Moore III 更新时间:8/27/2018 访问量:545

问:

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

写道

Scala 没有将协变与分配给 的 GLB ⊤ 统一,bcz afaics 在子类型“双统一”中分配的方向很重要。因此必须具有类型(即),同上类型,不能分别接受来自 或 的赋值。因此,价值限制问题起源于无方向的统一,而全球双统一被认为是不可判定的,直到上面链接的最新研究。List[A]List[Int]NoneOption[⊥]Option[Nothing]NilList[Nothing]Option[Int]List[Int]

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

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

编辑:我在上面的引文中表达的原始直觉(可以通过子类型来消除值限制)是不正确的。IMO 的答案很好地阐明了问题,我无法决定包含阿列克谢、安德烈亚斯或我的答案的集合中哪一个应该是选定的最佳答案。IMO,他们都是值得的。

Scala 子类型 Hindley-Milner 值限制

评论


答:

1赞 Shelby Moore III 2/3/2018 #1

编辑:这个答案以前是不正确的。我完全重写了下面的解释,以从安德烈亚斯和阿列克谢的答案下的评论中收集我的新理解。

archive.is 页的编辑历史和存档历史记录了我之前的误解和讨论。我选择编辑而不是删除和编写新答案的另一个原因是保留对此答案的评论。IMO,这个答案仍然是必要的,因为尽管阿列克谢正确、最简洁地回答了主题标题——安德烈亚斯的阐述也最有助于我获得理解——但我认为外行读者可能需要一个不同的、更全面(但希望仍然是生成本质)的解释,以便快速获得对这个问题的深度理解。此外,我认为其他答案掩盖了整体解释的复杂性,我希望天真的读者可以选择品尝它。我发现之前的解释并没有用英语陈述所有细节,而是(正如数学家为了提高效率而倾向于做的那样)依靠读者从符号编程语言示例和先决条件领域知识(例如,有关编程语言设计的背景事实)的细微差别中辨别细节。


当我们对引用的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)

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

出现打字复杂化是为了防止3 所述引用(及其指向的对象)的类型参数(又称类型变量)的(重新)量化(即绑定或确定)到一个类型,该类型在重用先前用不同类型量化的所述引用的实例时有所不同。

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

切线地,由于缺乏明确的通用量词∀(因为隐式的 rank-1 prenex 词法范围量化可以通过诸如 或 协程之类的结构从词法评估顺序中移除),并且当 ML 的值限制中可能出现不安全的情况时,可以说更大的不规则性(与 Scala 相比):let

安德烈亚斯写道

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

例如,对于类似于数学符号的 let 表达式,重用引用的对象是必需的,即使它们在子句中可能被多次词法替换,也应仅创建和计算一次替换。因此,例如,如果函数应用程序在子句中被计算为(无论是否在词法上),而替换的类型参数为每个应用程序重新量化(因为替换的实例化仅在函数应用程序中以词法形式进行),那么如果应用程序没有被强制只量化一次有问题的类型参数(即不允许有问题的类型),那么类型安全性可能会丢失参数为多态性)。inin

值限制是 ML 的折衷方案,旨在防止所有不安全的情况,同时防止一些(以前认为是罕见的)安全情况,从而简化类型系统。值限制被认为是一种更好的折衷方案,因为早期(过时的)更复杂的类型方法的经验没有限制任何或尽可能多的安全情况,导致命令式编程和纯函数式(又名应用式)编程之间的分叉,并泄露了 ML 函子模块中抽象类型的一些封装。我引用了一些来源并在这里进行了详细说明。不过,切线的是,我正在思考早期反对分叉的论点是否真的站得住脚,因为按名称调用根本不需要值限制(例如,当也被需要记忆时,Haskell 式的惰性评估),因为概念上部分的应用程序不会在已经评估的状态上形成闭包;模块化组合推理需要按名称调用,当与纯度结合使用时,则需要模块化(范畴理论方程推理)控制和效果组合。反对按名称调用的单态化限制论点实际上是关于强制类型注释,但是当需要最佳记忆(又称共享)时明确可以说不那么繁重,因为无论如何都需要该注释来实现模块化和可读性。按值调用是一种精细的齿梳级别的控制,因此,如果我们需要这种低级别的控制,那么也许我们应该接受值限制,因为更复杂的类型允许的极少数情况在命令式与应用式设置中不太有用。但是,我不知道是否可以以流畅/优雅的方式在相同的编程语言中将两者分层/隔离。代数效应可以在 CBV 语言(如 ML)中实现,它们可以消除值限制。哎呀,如果值限制影响了你的代码,可能是因为你的编程语言和库缺乏合适的元模型来处理效果

Scala 对所有此类引用进行了语法限制,这是一种折衷方案,它限制了与 ML 的值限制相同甚至更多的情况(如果不加以限制,这将是安全的),但从某种意义上说,它更常规,因为我们不会为限制相关的错误消息而挠头。在 Scala 中,我们永远不允许创建这样的引用。因此,在 Scala 中,我们只能表示在量化其类型参数时创建引用的新实例的情况。注意:在某些情况下OCaml 放宽了值限制。

注意:Scala 和 ML 都不支持声明引用是不可变的1,尽管它们指向的对象可以用 声明不可变。请注意,没有必要对无法更改的引用进行限制。val

为了使复杂的类型情况出现,需要引用类型1 的可变性,这是因为如果我们用非参数化对象(即不是 或 4,而是例如 a 或 ),那么引用将没有多态类型(与它所指向的对象有关),因此永远不会出现重新量化问题。因此,有问题的情况是由于使用多态对象进行实例化,然后随后在重新量化的上下文中分配一个新量化的对象(即改变引用类型),然后在随后的重新量化上下文中从(指向的对象)引用中取消引用(读取)。如前所述,当重新量化的类型参数发生冲突时,就会出现打字复杂情况,并且必须防止/限制不安全的情况。letNoneNilOption[String]List[Int]

唷!如果你在不查看链接示例的情况下理解了这一点,我会留下深刻的印象。


1 IMO 改用短语“可变引用”而不是“引用对象的可变性”和“引用类型的可变性”会更容易造成混淆,因为我们的目的是改变指针引用的对象值(及其类型),而不是引用指向的指针的可变性。一些编程语言甚至没有明确区分它们何时不允许在基元类型的情况下选择改变引用或它们指向的对象。

其中对象甚至可以是一个函数,在允许第一类函数的编程语言中。

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

4 在 ML 中分别为 NONE[]。

评论

1赞 Shelby Moore III 2/3/2018
@AluanHaddad提供类似 ML 的值限制并不是一个理想的功能。值限制是不希望的限制。所以“提供”不是正确的动词。我很欣赏你的评论,因为我可能应该澄清一下ML的价值限制是什么,以及它是对语言的不良限制。也许我会编辑这个问题。另外,直到最近我才对价值限制了解不多,我可能仍然一无所知。:-)
1赞 Aluan Haddad 2/3/2018
显示我知道多少......所以这就是让我的 F# 程序感到困惑的地方!谢谢你。我学到了一些有趣的东西。
1赞 Shelby Moore III 2/3/2018
@AluanHaddad,我在问题中添加了有关值限制的摘要。
0赞 Aluan Haddad 2/3/2018
优秀,阅读:)GitHub 上的有趣讨论也是如此。其中一些在我的脑海中很过分,但你对关闭提出了很多好的观点。就我个人而言,我认为它们是最有效的封装形式
1赞 Shelby Moore III 2/4/2018
许多错误和疏忽是存在的。欢迎专家评审。我不是专家,更像是煽动者或煽动者。:-)干杯。
2赞 Alexey Romanov 2/3/2018 #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 示例,你遇到的问题并不是缺少 : 与它完全对应。但是你需要类似的东西letval

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

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

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 中的多态值,而不是值限制允许的所有值。

评论

0赞 Alexey Romanov 2/3/2018
1. “但没有明确说明值受到限制” 它在“3.3 非值类型”下 2.“即 ⊥ 的子型和 ⊤ 的超型”正好相反 3. 不是推断的类型,它是它的一部分,就像不是类型一样。[A >: Nothing <: Any]Int =>
0赞 Alexey Romanov 2/3/2018
此外,还有带有子类型的 ML 版本,例如 lambda-the-ultimate.org/node/5393。它不会影响多态值:“由于 MLsub 的类型化规则只是具有额外 (SUB) 规则的 ML 的类型化规则,因此 ML 中可键入的任何表达式都可以在 MLsub 中具有相同类型的类型。
0赞 Shelby Moore III 2/3/2018
你写的“恰恰相反”,你指出了一个错别字,我把⊥和⊤换了。但这种更正并不能排除我的说法“无法填充”。当我之前回答时,我认为您可能指的是具有相反协方差限制方向的类型。刚刚注意到错别字。谢谢。然而,我在上面解释过,结合我的答案,没有办法构造一个值,其类型是 。正如你所暗示的,该类型仅在函数的上下文中才有意义。List[A]AList[A]A[A >: Nothing <: Any]
0赞 Alexey Romanov 2/4/2018
“ML类型不是多态值的类型”和“类型是”对我来说似乎是类别错误:甚至没有错。 并且是类型变量,而不是表达式,它们没有类型。'a list ref'aA[A >: Nothing <: Any]'aA
0赞 Alexey Romanov 2/4/2018
'a list但是,是多态值的类型(方案)。[]
4赞 Andreas Rossberg 2/4/2018 #3

正如我之前所解释的,当您将参数多态性与可变引用(或某些其他效果)相结合时,就需要值限制或类似的东西。这完全独立于语言是否具有类型推断,或者该语言是否也允许子类型。一个规范的计数器示例,例如

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

不受省略类型批注能力的影响,也不受向量化类型添加绑定的能力的影响。

因此,当您添加对 F<: 的引用时,您需要施加一个值限制,以免失去合理性。同样,MLsub 也无法摆脱值限制。Scala 已经通过其语法强制执行了值限制,因为甚至没有办法编写具有多态类型的值的定义。

评论

0赞 Shelby Moore III 2/4/2018
很抱歉争论不休,但 Scala 的语法并没有阻止我写作,而是类型检查器抱怨“未找到:类型 A”。然而,Scala 并没有强制执行 ML 中看到的其他值限制,例如当我在 REPL 中成功编译时观察到的那样。val r : List[A] = Nildef id[A](x:A):A = xdef f[A](x:A):A = id(id(x))
2赞 Andreas Rossberg 2/4/2018
@ShelbyMooreIII,你不能在 Scala 中编写的等效内容是 .表单始终定义一个函数,因此不需要任何进一步的限制。var r[A] : List[A] = Nildef
0赞 Shelby Moore III 2/4/2018
研究一个例子,我现在同意这个问题不是由于缺乏子类型、推理或注释而出现的,而仅仅是因为绑定允许在函数外部实例化(仅一次),但在函数的参数多态性内进行词法范围。也许这就是您在语法上启用“参数多态性与可变引用”的组合的意思?暗示 Scala 不是参数多态的?Scala 有可变的引用,那么 Scala 没有你的哪些标准呢?letr
0赞 Andreas Rossberg 2/4/2018
@ShelbyMooreIII,Scala 两者兼而有之,并且它有一个包含值限制的语法限制,请参阅上面的评论。
1赞 Andreas Rossberg 2/4/2018
@ShelbyMooreIII,我说 Scala 的语法限制包含了值限制,所以它甚至更强大:在 ML 中,我可以很好地定义为多态值,但在 Scala 中我不能。Monomorphic 完全没有重载,它由类型变量的绑定器/量词所在的位置定义。当某物具有量化类型时,它是多态的。不幸的是,ML 通常不会在其语法中明确量词,而仅在其类型规则中明确。let l = []