Skolemisierung existentiell typisierter Ausdrücke

In Scala löst der folgende Ausdruck einen Typfehler aus:

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

Wie in @ erwäh SI-9899 und dasAntworte, das ist richtig nach der Spezifikation:

Ich denke, dies funktioniert wie in SLS 6.1 beschrieben: "Die folgende Skolemisierungsregel gilt allgemein für jeden Ausdruck: Wenn der Typ eines Ausdrucks ein existentieller Typ T wäre, wird stattdessen angenommen, dass der Typ des Ausdrucks ein ist Skolemisierung von T. "

Das verstehe ich aber nicht ganz. An welchem Punkt wird diese Regel angewendet? Trifft dies in der ersten Zeile zu (d. H. Der Typ vonpair ist anders als in der Typanmerkung angegeben) oder in der zweiten Zeile (aber das Anwenden der Regel auf die zweite Zeile insgesamt würde nicht zu einem Typfehler führen)?

Nehmen wir an, SLS 6.1 gilt für die erste Zeile. Es soll skolemize existenzielle Typen. Wir können den in der ersten Zeile angegebenen Typ zu einem nicht existenziellen Typ machen, indem wir ihn in einen Typparameter einfügen:

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)

Es klappt! (Kein Tippfehler.) Das bedeutet, dass der existenzielle Typ "verloren" gegangen ist, als wir @ definiert habepair? Nein

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

Dieser Typ prüft! Wenn es der "Fehler" der Zuordnung zu @ gewesen wäpair, das sollte nicht funktionieren. Der Grund, warum es nicht funktioniert, liegt also in der zweiten Zeile. Wenn das der Fall ist, was ist der Unterschied zwischen demwrap und diepair Beispiel?

Zum Abschluss hier noch ein paar Beispiele:

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

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

Beide funktionieren nicht, aber in Analogie zu der Tatsache, dasswrap.x._1(wrap.x._2) tat typecheck, ich hätte gedacht, dassa2(b2) könnte auch typecheck sein.

Antworten auf die Frage(2)

Ihre Antwort auf die Frage