提问人:Shelby Moore III 提问时间:2/3/2018 最后编辑:Shelby Moore III 更新时间:8/27/2018 访问量:545
Scala 是否像 ML 一样有值限制,如果没有,那为什么?
Does Scala have a value restriction like ML, if not then why?
问:
以下是我对这个问题的看法。任何人都可以确认、否认或详细说明吗?
我写道:
Scala 没有将协变与分配给 的 GLB ⊤ 统一,bcz afaics 在子类型“双统一”中分配的方向很重要。因此必须具有类型(即),同上类型,不能分别接受来自 或 的赋值。因此,价值限制问题起源于无方向的统一,而全球双统一被认为是不可判定的,直到上面链接的最新研究。
List[A]
List[Int]
None
Option[⊥]
Option[Nothing]
Nil
List[Nothing]
Option[Int]
List[Int]
您可能希望查看上述评论的上下文。
ML 的值限制将不允许参数多态性在(以前认为很少见,但可能更普遍)的情况下这样做是合理的(即类型安全),例如特别是对于库里函数的部分应用(这在函数式编程中很重要),因为替代类型解决方案在函数式编程和命令式编程之间创建分层,以及模块化抽象类型的中断封装。Haskell具有类似的双重单态化限制。在某些情况下,OCaml 放宽了限制。我详细阐述了其中的一些细节。
编辑:我在上面的引文中表达的原始直觉(可以通过子类型来消除值限制)是不正确的。IMO 的答案很好地阐明了问题,我无法决定包含阿列克谢、安德烈亚斯或我的答案的集合中哪一个应该是选定的最佳答案。IMO,他们都是值得的。
答:
编辑:这个答案以前是不正确的。我完全重写了下面的解释,以从安德烈亚斯和阿列克谢的答案下的评论中收集我的新理解。
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)
所引用的对象中包含的值(类似于 )可以分配给具有类型参数的任何具体类型的引用,因为具有多态类型。这将允许类型不安全,因为如上面的示例所示,所引用的同一对象已被分配给两者,并且可以通过引用使用值写入(即突变),然后通过引用读取为值。对于上述示例,值限制会生成编译器错误。NONE
null
r
'a
r
a'
r
string option ref
int option ref
string
r1
int
r2
出现打字复杂化是为了防止3 所述引用(及其指向的对象)的类型参数(又称类型变量)的(重新)量化(即绑定或确定)到一个类型,该类型在重用先前用不同类型量化的所述引用的实例时有所不同。
例如,连续的函数应用程序(也称为调用)重用此类引用的相同实例时,就会出现这种(可以说是令人困惑和复杂的)情况。IOW,每次应用函数时,引用的类型参数(与对象相关)都会被(重新)量化,但引用(及其指向的对象)的相同实例被重用于函数的每个后续应用(和量化)。
切线地,由于缺乏明确的通用量词∀(因为隐式的 rank-1 prenex 词法范围量化可以通过诸如 或 协程之类的结构从词法评估顺序中移除),并且当 ML 的值限制中可能出现不安全的情况时,可以说更大的不规则性(与 Scala 相比):let
安德烈亚斯写道:
不幸的是,ML 通常不会在其语法中明确量词,而仅在其类型规则中明确。
例如,对于类似于
数学符号的 let 表达式,重用引用的对象是必需的,即使它们在子句中可能被多次词法替换,也应仅创建和计算一次替换。因此,例如,如果函数应用程序在子句中被计算为(无论是否在词法上),而替换的类型参数为每个应用程序重新量化(因为替换的实例化仅在函数应用程序中以词法形式进行),那么如果应用程序没有被强制只量化一次有问题的类型参数(即不允许有问题的类型),那么类型安全性可能会丢失参数为多态性)。in
in
值限制是 ML 的折衷方案,旨在防止所有不安全的情况,同时防止一些(以前认为是罕见的)安全情况,从而简化类型系统。值限制被认为是一种更好的折衷方案,因为早期(过时的)更复杂的类型方法的经验没有限制任何或尽可能多的安全情况,导致命令式编程和纯函数式(又名应用式)编程之间的分叉,并泄露了 ML 函子模块中抽象类型的一些封装。我引用了一些来源并在这里进行了详细说明。不过,切线的是,我正在思考早期反对分叉的论点是否真的站得住脚,因为按名称调用根本不需要值限制(例如,当也被需要记忆时,Haskell 式的惰性评估),因为概念上部分的应用程序不会在已经评估的状态上形成闭包;模块化组合推理需要按名称调用,当与纯度结合使用时,则需要模块化(范畴理论和方程推理)控制和效果组合。反对按名称调用的单态化限制论点实际上是关于强制类型注释,但是当需要最佳记忆(又称共享)时明确可以说不那么繁重,因为无论如何都需要该注释来实现模块化和可读性。按值调用是一种精细的齿梳级别的控制,因此,如果我们需要这种低级别的控制,那么也许我们应该接受值限制,因为更复杂的类型允许的极少数情况在命令式与应用式设置中不太有用。但是,我不知道是否可以以流畅/优雅的方式在相同的编程语言中将两者分层/隔离。代数效应可以在 CBV 语言(如 ML)中实现,它们可以消除值限制。哎呀,如果值限制影响了你的代码,可能是因为你的编程语言和库缺乏合适的元模型来处理效果。
Scala 对所有此类引用进行了语法限制,这是一种折衷方案,它限制了与 ML 的值限制相同甚至更多的情况(如果不加以限制,这将是安全的),但从某种意义上说,它更常规,因为我们不会为与值限制相关的错误消息而挠头。在 Scala 中,我们永远不允许创建这样的引用。因此,在 Scala 中,我们只能表示在量化其类型参数时创建引用的新实例的情况。注意:在某些情况下,OCaml 放宽了值限制。
注意:Scala 和 ML 都不支持声明引用是不可变的1,尽管它们指向的对象可以用 声明不可变。请注意,没有必要对无法更改的引用进行限制。val
为了使复杂的类型情况出现,需要引用类型1 的可变性,这是因为如果我们用非参数化对象(即不是 或 4,而是例如 a 或 ),那么引用将没有多态类型(与它所指向的对象有关),因此永远不会出现重新量化问题。因此,有问题的情况是由于使用多态对象进行实例化,然后随后在重新量化的上下文中分配一个新量化的对象(即改变引用类型),然后在随后的重新量化上下文中从(指向的对象)引用中取消引用(读取)。如前所述,当重新量化的类型参数发生冲突时,就会出现打字复杂情况,并且必须防止/限制不安全的情况。let
None
Nil
Option[String]
List[Int]
唷!如果你在不查看链接示例的情况下理解了这一点,我会留下深刻的印象。
1 IMO 改用短语“可变引用”而不是“引用对象的可变性”和“引用类型的可变性”会更容易造成混淆,因为我们的目的是改变指针引用的对象值(及其类型),而不是引用指向的指针的可变性。一些编程语言甚至没有明确区分它们何时不允许在基元类型的情况下选择改变引用或它们指向的对象。
其中,对象甚至可以是一个函数,在允许第一类函数的编程语言中。
3 为了防止在运行时由于访问(读取或写入)引用对象而导致分段错误,并假定其静态(即在编译时)确定的类型不是对象实际具有的类型。
4 在 ML 中分别为 NONE
和 []。
评论
这比这简单得多。在 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 => ... }
}
这是非法的。如果你写它是合法的,但在每次调用时都会创建一个新的。用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 中的多态值,而不是值限制允许的所有值。
评论
[A >: Nothing <: Any]
Int =>
List[A]
A
List[A]
A
[A >: Nothing <: Any]
'a list ref
'a
A
[A >: Nothing <: Any]
'a
A
'a list
但是,是多态值的类型(方案)。[]
正如我之前所解释的,当您将参数多态性与可变引用(或某些其他效果)相结合时,就需要值限制或类似的东西。这完全独立于语言是否具有类型推断,或者该语言是否也允许子类型。一个规范的计数器示例,例如
let r : ∀A.Ref(List(A)) = ref [] in
r := ["boo"];
head(!r) + 1
不受省略类型批注能力的影响,也不受向量化类型添加绑定的能力的影响。
因此,当您添加对 F<: 的引用时,您需要施加一个值限制,以免失去合理性。同样,MLsub 也无法摆脱值限制。Scala 已经通过其语法强制执行了值限制,因为甚至没有办法编写具有多态类型的值的定义。
评论
val r : List[A] = Nil
def id[A](x:A):A = x
def f[A](x:A):A = id(id(x))
var r[A] : List[A] = Nil
def
let
r
let l = []
评论