Systemy typów, II UWr, 2010/11
Lista zadań nr 4 (na 21 i 22 grudnia 2010)

Zadanie 1 (20p)

Zaimplementuj system typów oraz interpreter języka funkcyjnego z typami prostymi oraz podtypowaniem (w oparciu o semantykę inkluzyjną), zawierający:
  • wyrażenia arytmetyczne (typ Nat, stałe liczbowe w reprezentacji unarnej, podstawowe operacje arytmetyczne),
  • wyrażenia logiczne (typ Bool, stałe true i false, podstawowe operacje logiczne, w tym wyrażenie warunkowe, podstawowe relacje na wyrażeniach arytmetycznych),
  • wyrażenia napisowe (typ String, stałe napisowe, podstawowe operacje, np. konkatenacja napisów),
  • rachunek lambda,
  • rekordy,
  • wyrażenie letrec f (x : T) : S = t in t.

Uwagi:
  1. Zakładamy, że Bool <: Nat, Bool <: String i Nat <: String.
  2. Typowanie wyrażenia warunkowego if t1 then t2 else t3 wymaga wyznaczenia najmniejszego wspólnego nadtypu typów wyrażeń t2 i t3 ([Pie02]:16.3) - zaimplementuj operację wyznaczania takiego nadtypu.
  3. Interpereter może bazować na dowolnej semantyce operacyjnej CBV języka (SOS, semantyka naturalna, maszyna abstrakcyjna, semantyka redukcyjna).

Zadanie 2 (20p)

Zaimplementuj (napisz typechecker i interpreter) język Featherweight Java zgodnie z jego specyfikacją podaną w rozdziale 19 podręcznika [Pie02]. Rozszerzenie podstawowej implementacji o rozwiązanie któregoś z ćwiczeń 19.4.3, 19.4.4, 19.4.6 lub 19.4.7 będzie dodatkowo punktowane.

Zadanie 3 (dla chętnych, 20p)

Zaimplementuj język programowania (lub jakiś jego interesujący podzbiór) z Zadania 1 opierając się na (koherentnej) koercyjnej semantyce podtypowania.