存在类型表达式的Skolemization [英] Skolemization of existentially typed expressions

问题描述

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

In Scala, the following expression raises a type error:

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

如 SI-9899 所述，此

As mentioned in SI-9899 and this answer, this is correct according to the spec:

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

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的类型与类型注释所给出的类型不同)还是适用于第二行(但将规则整体应用于第二行不会导致类型错误)?

However, I do not fully understand this. At which point is this rule applied? Does it apply in the first line (i.e., the type of pair is a different one than given by the type annotation), or in the second line (but applying the rule to the second line as a whole would not lead to a type error)?

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

Let's assume SLS 6.1 applies to the first line. It is supposed to skolemize existential types. We can make the in the first line a non-existential type by putting the existential inside a type parameter:

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时，存在类型丢失"了吗?否:

It works! (No type error.) So that means, the existential type got "lost" when we defined pair? No:

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

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

This type checks! If it would have been the "fault" of the assignment to pair, this should not work. Thus, the reason why it does not work lies in the second line. If that's the case, what's the difference between the wrap and the pair example?

最后，这是另外一对示例:

To wrap up, here is one more pair of examples:

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

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

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

Both don't work, but by analogy to the fact that wrap.x._1(wrap.x._2) did typecheck, I would have thought that a2(b2) might typecheck, too.

推荐答案

我相信我已经弄清楚了整个过程中上述表达式的键入方式.

I believe I figured out most of the process how the expressions above are typed.

首先，这是什么意思:

以下skolemization规则普遍适用于每个 表达式:如果表达式的类型将是存在类型 T，则假定表达式的类型为a T的伪造. [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. [SLS 6.1]

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

It means that whenever an expression or subexpression is determined to have type T[A] forSome {type A}, then a fresh type name A1 is chosen, and the expression is given type T[A1]. This makes sense since T[A] forSome {type A} intuitively means that there is some type A such that the expression has type T[A]. (What name is chosen depends on the compiler implementation. I use A1 to distinguish it from the bound type variable A)

我们看一下第一行代码:

We look at the first line of code:

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)类型.

Here the skolemization rule is actually not yet used. ({ a: Int => a.toString }, 19) has type (Int=>String, Int). This is a subtype of (A => String, A) forSome { type A } since there exists an A (namely Int) such that the rhs is of type (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).

Now the typer assigns types to subexpressions from inside out. First, the first occurrence of pair is given a type. Recall that pair had type (A => String, A) forSome { type A }. Since the skolemization rule applies to every subexpression, we apply it to the first pair. We pick a fresh type name A1, and type pair as (A1 => String, A1). Then we assign a type to the second occurrence of pair. Again the skolemization rule applies, we pick another fresh type name A2, and the second occurrence of pair is types as (A2=>String,A2).

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

Then pair._1 has type A1=>String and pair._2 has type A2, thus pair._1(pair._2) is not well-typed.

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

Note that it is not the skolemization rule's "fault" that typing fails. If we would not have the skolemization rule, pair._1 would type as (A=>String) forSome {type A} and pair._2 would type as A forSome {type A} which is the same as Any. And then pair._1(pair._2) would still not be well-typed. (The skolemization rule is actually helpful in making things type, we will see that below.)

因此，为什么Scala拒绝理解pair的两个实例实际上是相同的A 的(A=>String,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可以更改内容，即从统一化到初始化.但是我不知道在这种情况下是否会导致问题.)

So, why does Scala refuse to understand that the two instances of pair actually are of type (A=>String,A) for the same A? I do not know a good reason in case of a val pair, but for example if we would have a var pair of the same type, the compiler must not skolemize several occurrences of it with the same A1. Why? Imagine that within an expression, the content of pair changes. First it contains an (Int=>String, Int), and then towards the end of the evaluation of the expression, it contains a (Bool=>String,Bool). This is OK if the type of pair is (A=>String,A) forSome {type A}. But if the computer would give both occurrences of pair the same skolemized type (A1=>String,A1), the typing would not be correct. Similarly, if pair would be a def pair, it could return different results on different invocations, and thus must not be skolemized with the same A1. For val pair, this argument does not hold (since val pair cannot change), but I assume that the type system would get too complicated if it would try to treat a val pair different from a var pair. (Also, there are situations where a val can change content, namely from unitialized to initialized. But I don't know whether that can lead to problems in this context.)

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

However, we can use the skolemization rule to make pair._1(pair._2) well-typed. A first try would be:

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

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

Why should this work? pair types as (A=>String,A) forSome {type A}. Thus it's type becomes (A3=>String,A3) for some fresh A3. So the new val pair2 should be given type (A3=>String,A3) (the type of the rhs). And if pair2 has type (A3=>String,A3), then pair2._1(pair2._2) will be well-typed. (No existentials involved any more.)

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

Unfortunately, this will actually not work, because of another rule in the spec:

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

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]

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

The packed type is the opposite of skolemization. That means, all the fresh variables that have been introduced inside the expression due to the skolemization rule are now transformed back into existential types. That is, T[A1] becomes T[A] forSome {type A}.

因此，在

val pair2 = pair

实际上，即使的类型是(A3=>String,A3)，

pair2也会被赋予类型(A=>String,A) forSome {type A}.如上所述，pair2._1(pair2._2)将不会输入.

pair2 will actually be given type (A=>String,A) forSome {type A} even though the rhs was given type (A3=>String,A3). Then pair2._1(pair2._2) will not type, as explained above.

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

But we can use another trick to achieve the desired result:

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，并且全部键入正确.

At the first glance, this is a pointless pattern match, since pair2 is just assigned pair, so why not just use pair? The reason is that the rule from SLS 4.1 only applied to vals and vars. Variable patterns (like pair2 here) are not affected. Thus pair is typed as (A4=>String,A4) and pair2 is given the same type (not the packed type). Then pair2._1 is typed A4=>String and pair2._2 is typed A4 and all is well-typed.

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

So a code fragment of the form x match { case x2 => can be used to "upgrade" x to a new "pseudo-value" x2 that can make some expressions well-typed that would not be well-typed using x. (I don't know why the spec does not simply allow the same thing to happen when we write val x2 = x. It would certainly be nicer to read since we do not get an extra level of indentation.)

这次游览之后，让我们浏览问题中其余表达式的输入:

After this excursion, let us go through the typing of the remaining expressions from the question:

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规则，因此对于新的A5，表达式(即Wrap的参数)的类型为(A5=>String,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}]！)请注意，通过运行带有选项-Xprint:typer的编译器，我们可以确认wrap具有这种类型.

Here the expression ({ a: Int => a.toString }, 19) types as (Int=>String,Int). The type case makes this into an expression of type (A => String, A) forSome { type A }). Then the skolemization rule is applied, so the expression (the argument of Wrap, that is) gets type (A5=>String,A5) for a fresh A5. We apply Wrap to it, and that the rhs has type Wrap[(A5=>String,A5)]. To get the type of wrap, we need to apply the rule from SLS 4.1 again: We compute the packed type of Wrap[(A5=>String,A5)] which is Wrap[(A=>String,A)] forSome {type A}. So wrap has type Wrap[(A=>String,A)] forSome {type A} (and not Wrap[(A=>String,A) forSome {type A}] as one might expect at the first glance!) Note that we can confirm that wrap has this type by running the compiler with option -Xprint:typer.

我们现在输入

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

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

Here the skolemization rule applies to both occurrences of wrap, and they get typed as Wrap[(A6=>String,A6)] and Wrap[(A7=>String,A7)], respectively. Then wrap.x._1 has type A6=>String, and wrap.x._2 has type A7. Thus wrap.x._1(wrap.x._2) is not well-typed.

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

But the compiler disagrees and accepts wrap.x._1(wrap.x._2)! I do not know why. Either there is some additional rule in the Scala type system that I don't know about, or it is simply a compiler bug. Running the compiler with -Xprint:typer does not give extra insight, either, since it does not annotate the subexpressions in 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具有相同的类型.

Here pair has type (A=>String,A) forSome {type A} and skolemizes to (A8=>String,A8). Then Wrap(pair) has type Wrap[(A8=>String,A8)] and wrap2 gets the packed type Wrap[(A=>String,A)] forSome {type A}. I.e., wrap2 has the same type as wrap.

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

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

As with wrap.x._1(wrap.x._2), this should not type but does.

val Wrap((a2,b2)) = wrap

在这里，我们看到了一条新规则:[

Here we see a new rule: [SLS 4.1] (not the part quoted above) explains that such a pattern match val statement is expanded to:

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

现在，我们可以看到(a2,b2)的A9类型为(A9=>String,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通过打包类型规则(与Any相同)获取A forSome {type A}类型.

Now we can see that (a2,b2) gets type (A9=>String,A9) for fresh A9, tmp gets type (A=>String,A) forSome A due to the packed type rule. Then tmp._1 gets type A10=>String using the skolemization rule, and val a2 gets type (A=>String) forSome {type A} by the packed type rule. And tmp._2 gets type A11 using the skolemization rule, and val b2 gets type A forSome {type A} by the packed type rule (this is the same as Any).

因此

a2(b2)

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

is not well-typed, because a2 gets type A12=>String and b2 gets type A13=>String from the skolemization rule.

类似地，

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)类型.

Then tmp2 gets type (A=>String,A) forSome {type A} by the packed type rule, and val a3 and val b3 get type (A=>String) forSome {type A} and A forSome {type A} (a.k.a. Any), respectively.

然后

a3(b3)

由于与a2(b2)并非相同而导致的类型不正确.

is not well-typed for the same reasons as a2(b2) wasn't.

这篇关于存在类型表达式的Skolemization的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！