存在型表达式的摩擦化

Question

在Scala中,以下表达式引发类型错误:

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

正如SI-9899和这个答案中所提到的,根据规范,这是正确的:

我认为这是按照SLS 6.1的设计工作的:"以下skolemization规则适用于每个表达式:如果表达式的类型是存在类型T,那么表达式的类型将被假定为skolemization T."

但是,我不完全理解这一点.此规则适用于哪一点？它是否适用于第一行(即,类型pair与类型注释给出的类型不同),或者在第二行中应用(但将规则应用于第二行作为整体不会导致类型错误) ？

我们假设SLS 6.1适用于第一行.它应该skolemize存在的类型.我们可以通过将存在性放在类型参数中来使第一行中的非存在类型:

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，则假定表达式的类型是 T 的 skolemization。[SLS 6.1]

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

我们看第一行代码：

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

这里实际上还没有使用 skolemization 规则。 ({ 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是 types as (A2=>String,A2)。

然后pair._1has typeA1=>String且pair._2has type A2，因此pair._1(pair._2)不是良好类型。

请注意，输入失败并不是 skolemization 规则的“错误”。如果我们没有 skolemization 规则，pair._1则将键入 as(A=>String) forSome {type A}并pair._2键入 as A forSome {type A}，这与 相同Any。然后pair._1(pair._2)仍然无法正确输入。（skolemization 规则实际上有助于使事物类型化，我们将在下面看到。）

那么，为什么 Scala 拒绝理解这两个实例实际上是相同的pair类型呢？对于 a ，我不知道有什么好的理由，但是例如，如果我们有相同类型的 a ，编译器不得将它的多次出现用相同的 skolemize 。为什么？想象一下，在一个表达式中，内容发生了变化。首先它包含一个，然后在表达式求值结束时，它包含一个。如果 的类型是，则这是可以的。但是，如果计算机给出了相同 skolemized type的两次出现，则键入将不正确。类似地， if是 a ，它可能在不同的调用中返回不同的结果，因此不得使用相同的 skolemized 。对于，这个参数不成立（因为不能改变），但我认为如果类型系统尝试处理与 a 不同的类型，它会变得太复杂。（此外，在某些情况下 a可以更改内容，即从初始化到初始化。但我不知道这是否会导致这种情况下的问题。）(A=>String,A)Aval pairvar pairA1pair(Int=>String, Int)(Bool=>String,Bool)pair(A=>String,A) forSome {type A}pair(A1=>String,A1)pairdef pairA1val pairval pairval pairvar pairval

但是，我们可以使用 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所以应该给new类型(A3=>String,A3)（rhs 的类型）。如果pair2有 type (A3=>String,A3)，那么pair2._1(pair2._2)将是类型良好的。（不再涉及存在主义。）

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

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

填充型与斯科莱姆化相反。这意味着，由于 skolemization 规则而在表达式中引入的所有新变量现在都转换回存在类型。即T[A1]变为T[A] forSome {type A}.

因此，在

val pair2 = pair

pair2(A=>String,A) forSome {type A}即使 rhs 被赋予 type ，实际上也会被赋予 type (A3=>String,A3)。然后pair2._1(pair2._2)就不会打字了，如上所述。

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

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

乍一看，这是一个毫无意义的模式匹配，因为pair2只是分配了pair，那么为什么不直接使用呢pair？原因是 SLS 4.1 中的规则仅适用于vals 和vars。可变模式（如此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)。类型 case 使其成为类型 的表达式 (A => String, A) forSome { type A })。然后应用 skolemization 规则，因此表达式（Wrap即 的参数）获取(A5=>String,A5)fresh 的类型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通过使用 option 运行编译器来确认是否具有这种类型-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有 type(A=>String,A) forSome {type A}并 skolemizes 为(A8=>String,A8)。然后Wrap(pair)有 typeWrap[(A8=>String,A8)]并wrap2获取打包的 type 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

现在我们可以看到，获取fresh 的(a2,b2)类型， 由于打包类型规则而获取类型。然后使用 skolemization 规则获取类型，并通过打包类型规则获取类型。并使用 skolemization 规则获取类型，并通过打包类型规则获取类型（这与 相同）。(A9=>String,A9)A9tmp(A=>String,A) forSome Atmp._1A10=>Stringval a2(A=>String) forSome {type A}tmp._2A11val b2A forSome {type A}Any

因此

a2(b2)

类型不正确，因为a2获取类型A12=>String并从 skolemization 规则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 a3val b3(A=>String) forSome {type A}A forSome {type A}Any

然后

a3(b3)

a2(b2)由于与未键入的原因相同，其类型不正确。