skolemizacja z egzystencjalnie wpisywanych wyrażeń

Question

w Scala, następujące wyrażenie zgłasza błąd typu:

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

Jak wspomniano w SI-9899 i to answer ta jest poprawna według specyfikacji:

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."

jednak , Nie w pełni to rozumiem. W którym momencie stosuje się tę zasadę? Czy ma zastosowanie w pierwszym wierszu (tzn. Typ pair jest inny niż podany w adnotacji typu) lub w drugim wierszu (ale zastosowanie reguły do ​​drugiej linii jako całości nie doprowadziłoby do błędu typu)?

Załóżmy, że SLS 6.1 dotyczy pierwszej linii. To ma być skolemize typów egzystencjalnych. Możemy w pierwszej linii utworzyć typ nieistniejący, umieszczając egzystencjalne wewnątrz parametru typu:

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) 

Działa! (Brak błędu typu.) Czyli oznacza to, że typ egzystencjalny został "utracony", gdy zdefiniowaliśmy pair? No:

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

Ten typ sprawdza! Jeśli byłaby to "wina" przypisania do pair, nie powinno to działać. Tak więc powód, dla którego nie działa, leży w drugiej linii. Jeśli tak, to jaka jest różnica między przykładem wrap a pair?

omotać, tutaj jest jeszcze jedna parę przykładów:

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

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

Oba nie działają, ale przez analogię do tego, że wrap.x._1(wrap.x._2) zrobił typecheck, myślałem, że może typecheck a2(b2) też .

Answer 1

Wierzę, że wymyśliłem większość procesu, w jaki sposób wyrażeń powyżej są wpisane.

Po pierwsze, co to oznacza:

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]

Oznacza to, że gdy wyrazem lub podwyrażenie jest zdeterminowana, aby mieć typ T[A] forSome {type A}, to świeża nazwa typu A1 zostanie wybrany, a wyrażenie jest podany typ T[A1]. Ma to sens, ponieważ od T[A] forSome {type A} intuicyjnie oznacza, że ​​istnieje pewien typ A taki, że wyrażenie ma typ T[A]. (Co to nazwa wybrana zależy od implementacji kompilatora używam A1 aby odróżnić go od związanego typu zmienna A.)

Patrzymy na pierwszej linii kodu:

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

Tutaj zasada skolemizacja jest rzeczywiście jeszcze nieużywane. ({ a: Int => a.toString }, 19) ma typ (Int=>String, Int). Jest to podtyp (A => String, A) forSome { type A }, ponieważ istnieje A (mianowicie Int) taki, że rhs jest typu (A=>String,A).

Wartość pair ma teraz typ (A => String, A) forSome { type A }.

Kolejna linia jest

pair._1(pair._2) 

Teraz typer przypisuje typy do podwyrażeń od wewnątrz na zewnątrz. Po pierwsze, pierwsze wystąpienie pair otrzymuje typ. Przypomnijmy, że pair miał typ (A => String, A) forSome { type A }. Ponieważ reguła skolemizacji dotyczy każdego podwyrażenia, stosujemy ją do pierwszego pair. Wybieramy świeżą nazwę typu A1 i wpisujemy pair jako (A1 => String, A1). Następnie przypisujemy typ do drugiego wystąpienia pair. Ponownie obowiązuje reguła skolemization, wybieramy inną świeżą nazwę typu A2, a drugie wystąpienie pair jest typu (A2=>String,A2).

Następnie pair._1 ma typ A1=>String i pair._2 ma typ A2, więc pair._1(pair._2) nie jest dobrze wpisane.

Należy zauważyć, że to nie "błąd" reguły skolemization, że pisanie nie powiedzie się. Gdybyśmy nie mieli reguły skolemization, pair._1 wpisałby jako (A=>String) forSome {type A} i pair._2 napisałaby jako A forSome {type A}, która jest taka sama jak Any. A następnie pair._1(pair._2) nadal nie będzie dobrze napisane. (Zasada skolemizacja jest rzeczywiście pomocne w podejmowaniu rzeczy typu, przekonamy się, że poniżej).

Więc dlaczego Scala odmówić zrozumieć, że te dwa przypadki pair faktycznie są typu (A=>String,A) dla samo A? Nie mam dobrego powodu w przypadku val pair, ale na przykład, gdybyśmy mieli var pair tego samego typu, kompilator nie może skolemize kilku wystąpień tego z tym samym A1. Czemu? Wyobraź sobie, że w wyrażeniu zmienia się zawartość pair. Najpierw zawiera ona (Int=>String, Int), a następnie pod koniec oceny wyrażenia zawiera ona (Bool=>String,Bool). Jest to OK, jeśli typ pair to (A=>String,A) forSome {type A}. Ale jeśli komputer poda oba wystąpienia pair ten sam skolemizowany typ (A1=>String,A1), pisanie nie będzie poprawne. Podobnie, gdyby pair byłby , mógłby zwrócić różne wyniki dla różnych wywołań, a zatem nie może być skolemizowany z tym samym A1. W przypadku val pair ten argument nie jest spełniony (ponieważ val pair nie można zmienić), ale zakładam, że system typu stałby się zbyt skomplikowany, gdyby próbował potraktować zmienną val pair inną niż var pair. (Są też sytuacje, w których val może zmieniać treść, od unitialized do initialized, ale nie wiem, czy może to prowadzić do problemów w tym kontekście.)

Możemy jednak użyć reguły skolemization, aby pair._1(pair._2) dobrze napisane. Pierwsza próba to:

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

Dlaczego to powinno działać? pair typy jako (A=>String,A) forSome {type A}. Tak więc jego typ staje się (A3=>String,A3) dla świeżego A3. Tak więc nowy val pair2 powinien otrzymać typ (A3=>String,A3) (typ rhs). A jeśli pair2 ma typ (A3=>String,A3), wtedy pair2._1(pair2._2) będzie dobrze wpisane. (Nie ma już żadnych egzystencji.)

Niestety, ten będzie faktycznie nie działa, bo innej reguły w spec:

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]

Zapakowany typ jest przeciwieństwem skolemizacja. Oznacza to, że wszystkie świeże zmienne, które zostały wprowadzone w wyrażeniu z powodu reguły skolemization, są teraz przekształcane z powrotem w typy egzystencjalne. Oznacza to, że T[A1] staje się T[A] forSome {type A}.

Zatem w

val pair2 = pair 

pair2 będą faktycznie dany typ (A=>String,A) forSome {type A} chociaż RHS został dany typ (A3=>String,A3). Wtedy pair2._1(pair2._2) nie będzie wpisywać, jak wyjaśniono powyżej.

Ale możemy użyć innej sztuczki, aby osiągnąć pożądany rezultat:

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

Na pierwszy rzut oka jest to bezcelowe wzór mecz, ponieważ pair2 jest tylko przypisane pair, więc dlaczego nie wystarczy użyć pair? Powodem jest to, że reguła z SLS 4.1 dotyczy tylko val s oraz var s. Nie ma to wpływu na zmienne wzorce (np. pair2). Tak więc pair jest typowane jako (A4=>String,A4) i pair2 otrzymuje ten sam typ (nie jest zapakowany). Następnie pair2._1 jest wpisywane jako A4=>String i pair2._2 jest wpisywane jako A4 i wszystko jest dobrze napisane.

Więc fragment kodu formularza x match { case x2 => mogą być wykorzystywane do „upgrade” x do nowej „pseudo-wartości” x2 że można dokonać pewnych wyrażeń wpisywanych dobrze, że nie byłoby dobrze wpisywanych za pomocą x. (Nie wiem, dlaczego specyfikacja nie pozwala po prostu na to samo, gdy piszemy val x2 = x. Byłoby z pewnością lepiej przeczytać, ponieważ nie mamy dodatkowego poziomu wcięcia.)

Po tej wycieczce, idźmy przez wpisywanie pozostałych wyrażeń z pytaniem:

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

Tutaj wyrażenie ({ a: Int => a.toString }, 19) typy jak (Int=>String,Int). Typ przypadku powoduje, że jest to wyrażenie typu (A => String, A) forSome { type A }). Następnie stosowana jest reguła skolemization, więc wyrażenie (argument o numerze Wrap) otrzymuje nazwę (A5=>String,A5) dla świeżego A5. Stosujemy do niego Wrap, a rhs ma typ Wrap[(A5=>String,A5)]. Aby uzyskać typ wrap, musimy ponownie zastosować regułę z SLS 4.1: Obliczamy typ spakowany Wrap[(A5=>String,A5)], który jest Wrap[(A=>String,A)] forSome {type A}. Tak więc wrap ma typ Wrap[(A=>String,A)] forSome {type A} (a nie Wrap[(A=>String,A) forSome {type A}], jakiego można się było spodziewać na pierwszy rzut oka!) Zauważ, że możemy potwierdzić, że wrap ma ten typ, uruchamiając kompilator z opcją -Xprint:typer.

Teraz wpisz

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

Tutaj zasada skolemizacja dotyczy obu wystąpień wrap, a oni się wpisane jako Wrap[(A6=>String,A6)] i Wrap[(A7=>String,A7)], odpowiednio.Następnie wrap.x._1 ma typ A6=>String, a wrap.x._2 ma typ A7. Tak więc wrap.x._1(wrap.x._2) nie jest dobrze wpisany.

Ale kompilator nie zgadza się i akceptuje wrap.x._1(wrap.x._2)! Nie wiem dlaczego. W systemie Scala istnieje jakaś dodatkowa zasada, o której nie wiem, lub jest to po prostu błąd kompilatora. Uruchamianie kompilatora przy użyciu -Xprint:typer nie zapewnia dodatkowego wglądu, ponieważ nie zawiera adnotacji do podwyrażeń w wrap.x._1(wrap.x._2).

Dalej jest:

val wrap2 = Wrap(pair) 

Tutaj pair ma typ (A=>String,A) forSome {type A} i skolemizes do (A8=>String,A8). Następnie Wrap(pair) ma typ Wrap[(A8=>String,A8)] i wrap2 dostaje pakowany typ Wrap[(A=>String,A)] forSome {type A}. Tj. wrap2 ma ten sam typ co wrap.

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

Tak jak w przypadku wrap.x._1(wrap.x._2), nie powinno się wpisywać, ale robi.

val Wrap((a2,b2)) = wrap 

Tutaj widzimy nową regułę: [SLS 4.1] (a nie część cytowany powyżej) wyjaśnia, że ​​taki wzór mecz val oświadczenie rozszerzony:

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

Teraz widzimy, że (a2,b2) dostaje typ (A9=>String,A9) dla świeżego A9, tmp otrzymuje typ (A=>String,A) forSome A ze względu na regułę typu upakowanego. Następnie tmp._1 dostaje typ A10=>String przy użyciu reguły skolemization, a val a2 dostaje typ (A=>String) forSome {type A} według reguły typu spakowanego. I tmp._2 otrzymuje typ A11 przy użyciu reguły skolemization, a val b2 otrzymuje typ A forSome {type A} według reguły typu upakowanego (jest to to samo, co Any).

Zatem

a2(b2) 

nie jest dobrze wpisany, ponieważ a2 dostaje wpisać A12=>String i b2 dostaje wpisać A13=>String z reguły skolemizacja.

Podobnie

val (a3,b3) = pair 

rozszerza się

val tmp2 = pair match { case (a3,b3) => (a3,b3) } 
val a3 = tmp2._1 
val b3 = tmp2._2 

Następnie tmp2 dostaje wpisać (A=>String,A) forSome {type A} przez zapakowany reguły typu, a val a3 i val b3 typu get (A=>String) forSome {type A} i A forSome {type A} (a.k.a. Any), odpowiednio.

Następnie

a3(b3) 

nie jest dobrze wpisane na tych samych powodów jak a2(b2) nie było.