5109637319

Komentarz: Istnieje wiele rozwiązań tego problemu, żadne jednak nie jest eleganckie. Konserwatywne rozszerzenie systemu Damasa-Milnera wymaga wprowadzenia dodatkowych zmiennych typowych (tzw. słabych typów) i mało intuicyjnych reguł typowania. Prostsze rozwiązanie (Andrew Wrighta) uszkadza system typów tak, że przestaje być dla niego słuszne twierdzenie o subject reduction dla reguły 77. W Haskellu problem znika, bo nie ma skutków ubocznych (choć pojawia się dla funkcji unsaf ePerf ormIO i nie jest dla niej w żaden sposób rozwiązany — funkcja ta pozwala zdefiniować funkcję cast : a —► f3).

Zadanie 6. Pokaż, że w języku z poprzedniego zadania można przywrócić niesprzecz-ność jeśli wprowadzimy nowy rodzaj zmiennych, nazwijmy je słabymi i oznaczmy ich zbiór przez W. Zmienne te nie mogą wystąpić w schemacie typu po kwantyfikatorze, tj. nie wolno ich generalizować w regule let nawet, jeśli nie występują w T. Warunek w regule let ma więc postać a — FV(ti) \ (FV(r) U X). Przyjmij, że typy mają teraz postać

(Weak a\,..., Weak a_n) => r w której prefiks wskazuje, które zmienne są słabe.

Zadanie 7. Zauważ, że rekonstrukcja typów z polimorfizmem parametrycznym „kłóci się” z przeciążaniem operatorów — pokaż że w następującym języku:

t ::= x | t\t2 | Ax.t | let x = t\ in \ n \ r \ t\ + t2 r ::= o. | T\ —> r₂ | Int | Float er ::= Va.r

z regułami typowania

r, x : Va.T b x : rfa/f']

r b ti : n r,x : Wf.Ti h <2 : T2

r h t : Ti —> T2 rhs:r₂ T \~ ts : T2

T, x : Ti h t : T2 r h Ax.t : Ti —» T2

let x = t\ in t2 : T2

T h t\ : Int rbt₂ : Int

a = FV(n) \ FV(r)

r\-t₁+t₂: Int

r b n : Int

r b t\ : Float r b t₂ : Float r b t\ + t₂ : Float

istnieją programy nie posiadające typu głównego. Jaki wpływ ma brak typu głównego na efektywność rekonstrukcji typów i możliwość rozdzielnej kompilacji?

Zadanie 8. Pokaż, że w języku z poprzedniego zadania można przywrócić istnienie typów głównych, jeżeli wprowadzimy dodatkowy rodzaj zmiennych, nazwijmy je numerycznymi, a ich zbiór oznaczmy przez Af. Pod zmienne te wolno podstawić jedynie stałe Int oraz Float. Przyjmij, że typy mają teraz postać

(Num a\,..., Num a_n) =3- r

w której prefiks wskazuje, które zmienne są numeryczne. Zauważ, że jesteśmy o krok od wynalezienia haskellowych klas typów.

3