In Scala löst der folgende Ausdruck einen Typfehler aus:
%Vor%Wie in SI-9899 und diesem Antwort , das ist korrekt nach der Spezifikation:
Ich denke, das funktioniert nach SLS 6.1: "Das Folgende Skolemisierungsregel wird universell für jeden Ausdruck angewendet: Wenn der Typ eines Ausdrucks wäre ein existentieller Typ T, dann der Typ von der Ausdruck wird stattdessen als Skolemisierung von T angenommen. "
Allerdings verstehe ich das nicht vollständig. Wann wird diese Regel angewendet? Gilt es in der ersten Zeile (dh der Typ von pair ist ein anderer Typ als der Typ Annotation) oder in der zweiten Zeile (aber die Regel auf die zweite Zeile als Ganzes anzuwenden würde nicht zu a führen Typfehler)?
Nehmen wir an, dass SLS 6.1 für die erste Zeile gilt. Es soll existentielle Typen skolemisieren. Wir können das in der ersten Zeile zu einem nicht-existentiellen Typ machen, indem wir das existentielle Element in einen Typparameter setzen:
%Vor% Es funktioniert! (Kein Typfehler.) Das heißt, dass der existentielle Typ "verloren" wurde, als wir pair definierten? Nein:
Dieser Typ prüft! Wenn es der "Fehler" der Zuweisung zu pair gewesen wäre, sollte dies nicht funktionieren. Der Grund, warum es nicht funktioniert, liegt in der zweiten Zeile. Wenn das der Fall ist, was ist der Unterschied zwischen dem wrap und dem pair Beispiel?
Zum Schluss noch ein paar Beispiele:
%Vor% Beide funktionieren nicht, aber in Analogie zu der Tatsache, dass wrap.x._1(wrap.x._2) typecheck gemacht hat, hätte ich auch gedacht, dass a2(b2) auch tasten könnte.
Ich glaube, ich habe den größten Teil des Prozesses herausgefunden, wie die obigen Ausdrücke eingegeben werden.
Erstens, was bedeutet das:
Die folgende Skolemisierungsregel wird universell für jeden angewendet Ausdruck: Wenn der Typ eines Ausdrucks ein existentieller Typ wäre T, dann wird angenommen, dass der Typ des Ausdrucks a ist Skolemisierung von T. [SLS 6.1]
Dies bedeutet, dass immer dann, wenn für einen Ausdruck oder Teilausdruck der Typ T[A] forSome {type A} festgelegt ist, ein neuer Typname A1 ausgewählt wird und der Ausdruck den Typ T[A1] erhält. Dies ist sinnvoll, da T[A] forSome {type A} intuitiv bedeutet, dass es einen Typ A gibt, so dass der Ausdruck den Typ T[A] hat. (Welcher Name gewählt wird, hängt von der Compilerimplementierung ab. Ich verwende A1 , um ihn von der gebundenen Typvariablen A zu unterscheiden)
Wir sehen uns die erste Codezeile an:
%Vor% Hier wird die Skolemisierungsregel tatsächlich noch nicht benutzt.
({ a: Int => a.toString }, 19) hat den Typ (Int=>String, Int) . Dies ist ein Subtyp von (A => String, A) forSome { type A } , da es eine A (nämlich Int ) gibt, so dass die rhs vom Typ (A=>String,A) ist.
Der Wert pair hat jetzt den Typ (A => String, A) forSome { type A } .
Die nächste Zeile ist
%Vor% Nun ordnet der Typ den Unterausdrücken Typen von innen nach außen zu. Zuerst wird dem ersten Vorkommen von pair ein Typ zugewiesen. Erinnern Sie sich, dass pair den Typ (A => String, A) forSome { type A } hatte. Da die Skolemisierungsregel für jeden Unterausdruck gilt, wenden wir sie auf die erste pair an. Wir wählen einen neuen Typ namens A1 und geben pair als (A1 => String, A1) ein. Dann weisen wir dem zweiten Vorkommen von pair einen Typ zu. Wiederum gilt die Skolemisierungsregel, wir wählen einen anderen frischen Typnamen A2 , und das zweite Vorkommen von pair ist types als (A2=>String,A2) .
Dann hat pair._1 den Typ A1=>String und pair._2 hat den Typ A2 , daher ist pair._1(pair._2) nicht gut typisiert.
Beachten Sie, dass es nicht der "Fehler" der Skolemisierungsregel ist, dass die Eingabe fehlschlägt. Wenn wir die Skolemisierungsregel nicht hätten, würde pair._1 als (A=>String) forSome {type A} und pair._2 als A forSome {type A} eingeben, was dasselbe ist wie Any . Und dann wäre pair._1(pair._2) immer noch nicht gut typisiert. (Die Skolemisierungsregel ist tatsächlich hilfreich, um die Dinge zu typisieren, wir werden das unten sehen.)
Also, warum weigert sich Scala zu verstehen, dass die beiden Instanzen von pair tatsächlich vom Typ (A=>String,A) für die gleiche A sind? Ich kenne keinen guten Grund im Falle von val pair , aber wenn wir zum Beispiel einen var pair vom gleichen Typ haben, darf der Compiler mehrere Vorkommen desselben mit demselben A1 nicht skolemisieren. Warum? Stellen Sie sich vor, dass sich der Inhalt von pair innerhalb eines Ausdrucks ändert. Zuerst enthält es ein (Int=>String, Int) und dann gegen Ende der Auswertung des Ausdrucks enthält es (Bool=>String,Bool) . Dies ist in Ordnung, wenn der Typ von pair (A=>String,A) forSome {type A} ist. Aber wenn der Computer beide Vorkommen von pair den gleichen skolemisierten Typ (A1=>String,A1) geben würde, wäre die Typisierung nicht korrekt. Ähnliches gilt, wenn pair ein def pair wäre, könnte es bei verschiedenen Aufrufen andere Ergebnisse liefern und daher nicht mit demselben A1 skolemisiert werden. Für val pair gilt dieses Argument nicht (da sich val pair nicht ändern kann), aber ich gehe davon aus, dass das Typsystem zu kompliziert wird, wenn es versuchen würde, eine val pair von einer var pair zu unterscheiden. (Es gibt auch Situationen, in denen ein val den Inhalt ändern kann, nämlich von unitialisiert zu initialisiert. Aber ich weiß nicht, ob das in diesem Zusammenhang zu Problemen führen kann.)
Allerdings können wir die Skolemisierungsregel verwenden, um pair._1(pair._2) gut typisiert zu machen. Ein erster Versuch wäre:
Warum sollte das funktionieren? pair types als (A=>String,A) forSome {type A} . Daher wird der Typ (A3=>String,A3) für einige frische A3 . Daher sollte der neue val pair2 den Typ (A3=>String,A3) (den Typ der rhs) erhalten. Und wenn pair2 den Typ (A3=>String,A3) hat, dann wird pair2._1(pair2._2) gut typisiert. (Keine Existenzen mehr beteiligt.)
Leider wird dies aufgrund einer anderen Regel in der Spezifikation nicht funktionieren:
Wenn die Wertdefinition nicht rekursiv ist, kann der Typ T weggelassen werden. in diesem Fall wird der gepackte Ausdruck e angenommen. [SLS 4.1]
Der gepackte Typ ist das Gegenteil von Skolemisierung. Das bedeutet, dass alle frischen Variablen, die aufgrund der Skolemisierungsregel in den Ausdruck eingefügt wurden, nun wieder in existentielle Typen umgewandelt werden. Das heißt, T[A1] wird T[A] forSome {type A} .
Also, in
%Vor% pair2 wird tatsächlich den Typ (A=>String,A) forSome {type A} erhalten, obwohl die rhs den Typ (A3=>String,A3) erhalten hat. Dann wird pair2._1(pair2._2) nicht wie oben beschrieben eingeben.
Aber wir können einen anderen Trick verwenden, um das gewünschte Ergebnis zu erzielen:
%Vor% Auf den ersten Blick ist dies eine sinnlose Musterübereinstimmung, da pair2 nur pair zugewiesen wurde. Warum also nicht einfach pair ?Der Grund dafür ist, dass die Regel aus SLS 4.1 nur auf val s und var s angewendet wurde. Variable Muster (wie pair2 hier) sind nicht betroffen. Daher wird pair als (A4=>String,A4) und pair2 als gleicher Typ (nicht als gepackter Typ) eingegeben. Dann wird pair2._1 typisiert A4=>String und pair2._2 ist typisiert A4 und alles ist gut typisiert.
Also kann ein Code-Fragment der Form x match { case x2 => verwendet werden, um x auf einen neuen "Pseudo-Wert" x2 zu "upgraden", was einige Ausdrücke gut typisiert, die nicht gut typisiert werden %Code%. (Ich weiß nicht, warum die Spezifikation nicht einfach das Gleiche zulässt, wenn wir x schreiben. Es wäre sicherlich angenehmer zu lesen, da wir keine zusätzliche Einrückungsebene erhalten.)
Lasst uns nach dieser Exkursion die folgenden Ausdrücke aus der Frage eingeben:
%Vor% Hier der Ausdruck val x2 = x types als ({ a: Int => a.toString }, 19) . Der Typ case macht dies zu einem Ausdruck des Typs
%Code%. Dann wird die Skolemisierungsregel angewendet, also erhält der Ausdruck (das Argument von (Int=>String,Int) ) den Typ (A => String, A) forSome { type A }) für ein neues Wrap . Wir wenden (A5=>String,A5) darauf an, und dass die rhs den Typ A5 hat. Um den Typ von Wrap zu erhalten, müssen wir die Regel aus SLS 4.1 erneut anwenden: Wir berechnen den gepackten Typ von Wrap[(A5=>String,A5)] , der wrap ist. Also Wrap[(A5=>String,A5)] hat den Typ Wrap[(A=>String,A)] forSome {type A} (und nicht wrap , wie man es auf den ersten Blick erwarten würde!) Beachten Sie, dass Wrap[(A=>String,A)] forSome {type A} diesen Typ hat, indem Sie den Compiler mit der Option Wrap[(A=>String,A) forSome {type A}] ausführen.
Wir tippen jetzt
%Vor% Hier gilt die Skolemisierungsregel für beide Vorkommen von wrap , und sie werden als -Xprint:typer bzw. wrap eingegeben. Dann hat Wrap[(A6=>String,A6)] den Typ Wrap[(A7=>String,A7)] und wrap.x._1 den Typ A6=>String . Daher ist wrap.x._2 nicht gut typisiert.
Aber der Compiler stimmt nicht zu und akzeptiert A7 ! Keine Ahnung warum. Entweder gibt es eine zusätzliche Regel im Scala-System, von der ich nichts weiß, oder es ist einfach ein Compiler-Bug. Das Ausführen des Compilers mit wrap.x._1(wrap.x._2) gibt auch keinen zusätzlichen Einblick, da die Unterausdrücke in wrap.x._1(wrap.x._2) nicht mit Anmerkungen versehen werden.
Weiter ist:
%Vor% Hier hat -Xprint:typer den Typ wrap.x._1(wrap.x._2) und skolemisiert sich auf pair . Dann hat (A=>String,A) forSome {type A} den Typ (A8=>String,A8) und Wrap(pair) den gepackten Typ Wrap[(A8=>String,A8)] . Das heißt, wrap2 hat denselben Typ wie Wrap[(A=>String,A)] forSome {type A} .
Wie bei wrap2 sollte dies nicht tippen, tut es aber.
Hier sehen wir eine neue Regel: [ SLS 4.1 ] (nicht der oben genannte Teil) erklärt, dass eine solche Musterübereinstimmung wrap -Anweisung auf Folgendes erweitert wird:
Jetzt können wir sehen, dass wrap.x._1(wrap.x._2) den Typ val für frische (a2,b2) bekommt,
(A9=>String,A9) erhält den Typ A9 aufgrund der Regel für den gepackten Typ. Dann erhält tmp den Typ (A=>String,A) forSome A mit der Skolemisierungsregel und tmp._1 den Typ A10=>String mit der Regel des gepackten Typs. Und val a2 erhält den Typ (A=>String) forSome {type A} mit der Skolemisierungsregel und tmp._2 erhält den Typ A11 mit der Regel des gepackten Typs (das ist das gleiche wie val b2 ).
Also
%Vor% ist nicht gut typisiert, weil A forSome {type A} den Typ Any und a2 den Typ A12=>String von der Skolemisierungsregel erhält.
Ähnlich,
%Vor%wird zu
erweitert %Vor% Dann wird b2 vom Typ gepackter Typ den Typ A13=>String erhalten, und tmp2 und (A=>String,A) forSome {type A} erhalten den Typ val a3 bzw. val b3 (a.k.a. (A=>String) forSome {type A} ).
Dann
%Vor% ist aus den gleichen Gründen nicht gut typisiert wie A forSome {type A} nicht.
Tags und Links scala existential-type