scala - 存在类型表达式的Skolemization

Question

在Scala中，以下表达式引发类型错误：

val pair: (A => String, A) forSome { type A } = ( { a: Int => a.toString }, 19 )
pair._1(pair._2)

如 SI-9899和此 answer中所述，根据规范，这是正确的：


我认为这是按照SLS 6.1设计的：
skolemization规则普遍适用于每个表达式：
表达式的类型将是存在类型T，然后是
该表达式被假定为T的假名。”


但是，我对此并不完全理解。在什么时候应用此规则？它适用于第一行（即 pair的类型与类型注释所给的类型不同）还是第二行（但将规则整体应用于第二行不会导致类型错误）？

假设SLS 6.1适用于第一行。应该是 skolemize存在类型。我们可以在第一行中通过将existential放入类型参数中来使其成为不存在的类型：

case class Wrap[T](x:T)
val wrap = Wrap(( { a: Int => a.toString }, 19 ) : (A => String, A) forSome { type A })
wrap.x._1(wrap.x._2)

有用！ （没有类型错误。）这就是说，当我们定义 pair时，存在类型“丢失”了吗？没有：

val wrap2 = Wrap(pair)
wrap2.x._1(wrap2.x._2)

此类型检查！如果这是 pair分配的“错误”，则此方法不起作用。因此，其不起作用的原因在于第二行。如果是这样的话， wrap和 pair示例之间有什么区别？

总结一下，这是另外一对示例：

val Wrap((a2,b2)) = wrap
a2(b2)

val (a3,b3) = pair
a3(b3)

两者都不起作用，但以类似于 wrap.x._1(wrap.x._2)进行类型检查的事实为例，我以为 a2(b2)也可能进行类型检查。

Answer 1

我相信我在整个过程中都弄清楚了上面的表达式是如何键入的。

首先，这是什么意思：


以下skolemization规则普遍适用于每个
表达式：如果表达式的类型将是存在类型
T，则假定表达式的类型为a
T. [SLS 6.1]的假名


这意味着只要确定一个表达式或子表达式的类型为T[A] forSome {type A}，就会选择一个新的类型名称A1，并且为表达式指定类型为T[A1]。这是有道理的，因为T[A] forSome {type A}直观地表示存在某种A类型，使得表达式具有类型T[A]。 （选择的名称取决于编译器的实现。我使用A1将其与绑定类型变量A区别开来）

我们看一下第一行代码：

val pair: (A => String, A) forSome { type A } = ({ a: Int => a.toString }, 19)

在这里，实际上尚未使用过死刑规则。
({ a: Int => a.toString }, 19)具有类型 (Int=>String, Int)。这是 (A => String, A) forSome { type A }的子类型，因为存在 A（即 Int），使得rhs是 (A=>String,A)类型。

值 pair现在具有类型 (A => String, A) forSome { type A }。

下一行是

pair._1(pair._2)

现在，打字员从内而外将类型分配给子表达式。首先，为 pair的第一次出现指定类型。回想一下 pair的类型是 (A => String, A) forSome { type A }。由于skolemization规则适用于每个子表达式，因此我们将其应用于第一个 pair。我们选择一个新的类型名称 A1，然后将 pair键入为 (A1 => String, A1)。然后，我们为 pair的第二次出现分配类型。再次使用skolemization规则，我们选择另一个新的类型名称 A2，第二次出现的 pair是类型为 (A2=>String,A2)的类型。

然后 pair._1的类型为 A1=>String， pair._2的类型为 A2，因此 pair._1(pair._2)的类型不正确。

请注意，键入失败不是归因于规则的“故障”。如果我们没有skolemization规则，则 pair._1将键入 (A=>String) forSome {type A}，而 pair._2将键入 A forSome {type A}，与 Any相同。然后 pair._1(pair._2)仍然不会被很好地键入。 （skolemization规则实际上有助于使事物类型化，我们将在下面看到。）

那么，为什么Scala拒绝理解 pair的两个实例实际上是同一 (A=>String,A)类型的 A？对于 val pair，我不知道有什么充分的理由，但是例如，如果我们有相同类型的 var pair，则编译器一定不能用相同的 A1来使它多次出现。为什么？想象一下，在表达式中， pair的内容会更改。首先，它包含一个 (Int=>String, Int)，然后在表达式求值的最后，它包含一个 (Bool=>String,Bool)。如果 pair的类型为 (A=>String,A) forSome {type A}，则可以。但是，如果计算机将两次出现的 pair赋予相同的斯科派字符类型 (A1=>String,A1)，则键入将不正确。同样，如果 pair将是 def pair，则在不同的调用下它可能返回不同的结果，因此，不得将其与相同的 A1一起使用。对于 val pair，此参数不成立（因为 val pair无法更改），但是我认为如果类型系统尝试将 val pair与 var pair区别对待，它将变得太复杂。 （此外，在某些情况下， val可以更改内容，即从统一化到初始化。但是我不知道在这种情况下是否会导致问题。）

但是，我们可以使用skolemization规则来使 pair._1(pair._2)正确键入。第一次尝试是：

val pair2 = pair
pair2._1(pair2._2)

为什么要这样做？ pair键入为 (A=>String,A) forSome {type A}。因此，对于某些新的 (A3=>String,A3)，其类型变为 A3。因此，应为新的 val pair2指定类型 (A3=>String,A3)（rhs的类型）。如果 pair2的类型为 (A3=>String,A3)，则 pair2._1(pair2._2)将被正确键入。 （不再涉及任何存在物。）

不幸的是，由于规范中的另一条规则，这实际上是行不通的：


如果值定义不是递归的，则可以省略类型T，
在这种情况下，假定表达式的压缩类型为e。 [SLS 4.1]


压缩类型与skolemization相反。这意味着，由于skolemization规则而已在表达式内部引入的所有新变量现在都将转换回存在类型。即， T[A1]变为 T[A] forSome {type A}。

因此，在

val pair2 = pair

实际上，即使rhs的类型为 pair2， (A=>String,A) forSome {type A}的类型也实际上为 (A3=>String,A3)。然后，如上所述， pair2._1(pair2._2)将不会键入。

但是我们可以使用另一个技巧来达到预期的结果：

pair match { case pair2 =>
  pair2._1(pair2._2) }

乍一看，这是毫无意义的模式匹配，因为 pair2只是分配了 pair，所以为什么不只使用 pair呢？原因是SLS 4.1中的规则仅适用于 val和 var。可变模式（如此处的 pair2）不受影响。因此，将 pair键入为 (A4=>String,A4)，并且 pair2被赋予相同的类型（而不是打包类型）。然后，将 pair2._1键入为 A4=>String，并且将 pair2._2键入为 A4，并且全部键入正确。

因此，形式为 x match { case x2 =>的代码片段可用于“升级” x到新的“伪值” x2，这可以使某些表达式具有良好的类型化，而使用 x不能很好地进行类型化。 （我不知道为什么规范在编写 val x2 = x时不只允许发生相同的事情。读起来肯定会更好，因为我们没有获得额外的缩进级别。）

游览之后，让我们遍历问题中其余的表达式：

val wrap = Wrap(({ a: Int => a.toString }, 19) : (A => String, A) forSome { type A })

在这里，表达式 ({ a: Int => a.toString }, 19)键入为 (Int=>String,Int)。类型的情况使它成为类型的表达式
(A => String, A) forSome { type A })。然后应用skolemization规则，因此表达式（即 Wrap的自变量）对于新的 (A5=>String,A5)获取类型 A5。我们对其应用 Wrap，并且rhs类型为 Wrap[(A5=>String,A5)]。要获取 wrap的类型，我们需要再次应用SLS 4.1中的规则：我们计算 Wrap[(A5=>String,A5)]的打包类型为 Wrap[(A=>String,A)] forSome {type A}。因此， wrap具有类型 Wrap[(A=>String,A)] forSome {type A}（而不是乍看之下的 Wrap[(A=>String,A) forSome {type A}]！）请注意，通过运行带有选项 wrap的编译器，我们可以确认 -Xprint:typer具有这种类型。

我们现在输入

wrap.x._1(wrap.x._2)

这里的skolemization规则适用于 wrap的两次出现，它们分别被键入为 Wrap[(A6=>String,A6)]和 Wrap[(A7=>String,A7)]。然后， wrap.x._1具有类型 A6=>String，而 wrap.x._2具有类型 A7。因此 wrap.x._1(wrap.x._2)的类型不正确。

但是编译器不同意并接受 wrap.x._1(wrap.x._2)！我不知道为什么。我不知道在Scala类型系统中还有一些其他规则，或者仅仅是一个编译器错误。使用 -Xprint:typer运行编译器也不会提供额外的见解，因为它不会注释 wrap.x._1(wrap.x._2)中的子表达式。

接下来是：

val wrap2 = Wrap(pair)

在这里 pair的类型为 (A=>String,A) forSome {type A}，并被伪装为 (A8=>String,A8)。然后 Wrap(pair)具有类型 Wrap[(A8=>String,A8)]，而 wrap2获得打包类型 Wrap[(A=>String,A)] forSome {type A}。即 wrap2具有与 wrap相同的类型。

wrap2.x._1(wrap2.x._2)

与 wrap.x._1(wrap.x._2)一样，它不应键入，但可以键入。

val Wrap((a2,b2)) = wrap

在这里，我们看到了一条新规则：[ SLS 4.1]（不是上面引用的部分）说明了将这种模式匹配 val语句扩展为：

val tmp = wrap match { case Wrap((a2,b2)) => (a2,b2) }
val a2 = tmp._1
val b2 = tmp._2

现在我们可以看到 (a2,b2)为新的 (A9=>String,A9)获取类型 A9，
由于打包的类型规则， tmp的类型为 (A=>String,A) forSome A。然后 tmp._1使用skolemization规则获取类型 A10=>String，而 val a2通过打包类型规则获取类型 (A=>String) forSome {type A}。并且 tmp._2使用skolemization规则获取类型 A11，而 val b2通过打包类型规则获取 A forSome {type A}类型（与 Any相同）。

从而

a2(b2)

的类型不正确，因为从skolemization规则中 a2的类型为 A12=>String，而 b2的类型为 A13=>String。

同样，

val (a3,b3) = pair

扩展到

val tmp2 = pair match { case (a3,b3) => (a3,b3) }
val a3 = tmp2._1
val b3 = tmp2._2

然后 tmp2根据打包类型规则获得类型 (A=>String,A) forSome {type A}，并且 val a3和 val b3分别获得类型 (A=>String) forSome {type A}和 A forSome {type A}（又称为 Any）。

然后

a3(b3)

由于 a2(b2)并非如此，因此类型不正确。