存在类型表达式的 Skolemization
Skolemization of existentially typed expressions
在 Scala 中，以下表达式引发类型错误：
val pair: (A => String, A) forSome { type A } = ( { a: Int => a.toString }, 19 )
pair._1(pair._2)
如 SI-9899 and this 中所述，根据规范这是正确的：
I think this is working as designed as per SLS 6.1: "The following
skolemization rule is applied universally for every expression: If the
type of an expression would be an existential type T, then the type of
the expression is assumed instead to be a skolemization of 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 时，存在类型得到 "lost"？否：
val wrap2 = Wrap(pair)
wrap2.x._1(wrap2.x._2)
此类型检查！如果它本来是赋值给 pair 的 "fault"，这应该不起作用。因此，它不起作用的原因在于第二行。如果是这样，wrap 和 pair 示例之间有什么区别？
总结一下，这里还有一对例子：
val Wrap((a2,b2)) = wrap
a2(b2)
val (a3,b3) = pair
a3(b3)
两者都不起作用，但是类比 wrap.x._1(wrap.x._2) 进行了类型检查，我本以为 a2(b2) 也可以进行类型检查。
我相信我已经弄清楚了上面的表达式是如何输入的大部分过程。
首先，这是什么意思：
The following skolemization rule is applied universally for every
expression: If the type of an expression would be an existential type
T, then the type of the expression is assumed instead to be a
skolemization of 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)
这里实际上还没有使用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 规则，我们选择另一个 fresh 类型名称 A2，第二次出现 pair 的类型为 (A2=>String,A2).
那么 pair._1 的类型为 A1=>String 而 pair._2 的类型为 A2，因此 pair._1(pair._2) 的类型不正确。
请注意，打字失败不是 skolemization 规则的 "fault"。如果我们没有 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，编译器不能用相同的 [=26] 对它的多次出现进行 skolemize =].为什么？想象一下，在一个表达式中，pair 的内容发生了变化。首先它包含一个 (Int=>String, Int)，然后在表达式计算结束时，它包含一个 (Bool=>String,Bool)。如果 pair 的类型是 (A=>String,A) forSome {type A}，这是可以的。但是，如果计算机将两次出现的 pair 都赋予相同的 skolemized 类型 (A1=>String,A1)，则键入将不正确。类似地，如果 pair 是 def pair，它可能 return 不同调用的不同结果，因此不能用相同的 A1 进行 skolemized。对于 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) 就是类型正确的。 （不再涉及存在主义。）
不幸的是，这实际上行不通，因为规范中的另一条规则：
If the value definition is not recursive, the type T may be omitted,
in which case the packed type of expression e is assumed. [SLS 4.1]
packed type与skolemization相反。这意味着，由于 skolemization 规则而在表达式中引入的所有新变量现在都被转换回存在类型。即 T[A1] 变为 T[A] forSome {type A}.
因此，在
val pair2 = pair
pair2 实际上将被赋予类型 (A=>String,A) forSome {type A}，即使 rhs 被赋予类型 (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 =>形式的代码片段可以用来"upgrade"x到新的"pseudo-value"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)。类型案例使 this 成为类型的表达式
(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}]！）请注意，我们可以通过 [=268= 来确认 wrap 的类型是 Wrap[(A=>String,A)] forSome {type A} ] 带有选项 -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} 并且 skolemizes 为 (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 通过 packed 类型规则获取类型 A forSome {type A}（这与 Any 相同）。
因此
a2(b2)
类型不正确，因为 a2 从 skolemization 规则获取类型 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}（ a.k.a.Any), 分别.
然后
a3(b3)
的类型不正确，原因与 a2(b2) 的类型相同。
在 Scala 中，以下表达式引发类型错误：
val pair: (A => String, A) forSome { type A } = ( { a: Int => a.toString }, 19 )
pair._1(pair._2)
如 SI-9899 and this
I think this is working as designed as per SLS 6.1: "The following skolemization rule is applied universally for every expression: If the type of an expression would be an existential type T, then the type of the expression is assumed instead to be a skolemization of 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 时，存在类型得到 "lost"？否：
val wrap2 = Wrap(pair)
wrap2.x._1(wrap2.x._2)
此类型检查！如果它本来是赋值给 pair 的 "fault"，这应该不起作用。因此，它不起作用的原因在于第二行。如果是这样，wrap 和 pair 示例之间有什么区别？
总结一下，这里还有一对例子：
val Wrap((a2,b2)) = wrap
a2(b2)
val (a3,b3) = pair
a3(b3)
两者都不起作用，但是类比 wrap.x._1(wrap.x._2) 进行了类型检查，我本以为 a2(b2) 也可以进行类型检查。
我相信我已经弄清楚了上面的表达式是如何输入的大部分过程。
首先，这是什么意思：
The following skolemization rule is applied universally for every expression: If the type of an expression would be an existential type T, then the type of the expression is assumed instead to be a skolemization of 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)
这里实际上还没有使用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 规则，我们选择另一个 fresh 类型名称 A2，第二次出现 pair 的类型为 (A2=>String,A2).
那么 pair._1 的类型为 A1=>String 而 pair._2 的类型为 A2，因此 pair._1(pair._2) 的类型不正确。
请注意，打字失败不是 skolemization 规则的 "fault"。如果我们没有 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，编译器不能用相同的 [=26] 对它的多次出现进行 skolemize =].为什么？想象一下，在一个表达式中，pair 的内容发生了变化。首先它包含一个 (Int=>String, Int)，然后在表达式计算结束时，它包含一个 (Bool=>String,Bool)。如果 pair 的类型是 (A=>String,A) forSome {type A}，这是可以的。但是，如果计算机将两次出现的 pair 都赋予相同的 skolemized 类型 (A1=>String,A1)，则键入将不正确。类似地，如果 pair 是 def pair，它可能 return 不同调用的不同结果，因此不能用相同的 A1 进行 skolemized。对于 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) 就是类型正确的。 （不再涉及存在主义。）
不幸的是，这实际上行不通，因为规范中的另一条规则：
If the value definition is not recursive, the type T may be omitted, in which case the packed type of expression e is assumed. [SLS 4.1]
packed type与skolemization相反。这意味着，由于 skolemization 规则而在表达式中引入的所有新变量现在都被转换回存在类型。即 T[A1] 变为 T[A] forSome {type A}.
因此，在
val pair2 = pair
pair2 实际上将被赋予类型 (A=>String,A) forSome {type A}，即使 rhs 被赋予类型 (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 =>形式的代码片段可以用来"upgrade"x到新的"pseudo-value"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)。类型案例使 this 成为类型的表达式
(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}]！）请注意，我们可以通过 [=268= 来确认 wrap 的类型是 Wrap[(A=>String,A)] forSome {type A} ] 带有选项 -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} 并且 skolemizes 为 (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 通过 packed 类型规则获取类型 A forSome {type A}（这与 Any 相同）。
因此
a2(b2)
类型不正确，因为 a2 从 skolemization 规则获取类型 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}（ a.k.a.Any), 分别.
然后
a3(b3)
的类型不正确，原因与 a2(b2) 的类型相同。