Systemy typów, II UWr, 2010/11
Lista zadań nr 3 (na 30.11.2010, 01.12.2010, 07.12.2010 i 08.12.2010)

Zadanie 1 (25p)

Zaimplementuj język funkcyjny z typami prostymi zdefiniowany w rozdziałach 8-11 podręcznika do wykładu [Pie:02]. Język ten zawiera:
  • wyrażenia arytmetyczne i logiczne (8),
  • rachunek lambda w reprezentacji z nazwami zmiennych (9),
  • typ Unit oraz sekwencję wyrażeń (11.2-11.3),
  • anotacje typowe (11.4),
  • definicje lokalne (11.5),
  • n-tki (11.6-11.7),
  • rekordy wraz z konstrukcją dopasowania wzorca (11.8),
  • warianty (11.9-11.10),
  • rekursję w postaci operatora punktu stałego i rekurencyjnych definicji lokalnych z użyciem wyrażenia letrec (11.11),
  • listy (11.12).
Napisz parser, funkcje drukujące w czytelny sposób wyrażenia oraz typy, funkcję sprawdzającą typ poprawnie zbudowanego wyrażenia oraz ewaluator implementujący semantykę małych kroków dla dobrze typowanych wyrażeń. Zbuduj bogaty zestaw testów.

Uwagi:
  1. Wyrażenia wyprowadzalne z innych, takie jak sekwencja wyrażeń czy letrec należy potraktować jak cukier syntaktyczny i przetłumaczyć w trakcie parsowania.
  2. Postaraj się ograniczyć wymagania dotyczące anotacji typowych wyrażeń do niezbędnego minimum (dotyczy szczególnie list).
  3. Mile widziane będą dokładne komunikaty o błędach składni i typów.
  4. Dla wygody programisty warto pozwolić mu na globalne definicje identyfikatorów postaci x = t. Definicja taka powoduje rozszerzenie globalnego środowiska zmiennych o wartość termu t. Jeżeli dopuścimy takie definicje, to semantyka małych kroków jest opisana przez relację ρ ⊢ t ⇒v t', powstałą z podanej w podręczniku relacji t ⇒ t' przez uwzględnienie środowiska ρ globalnie zdefiniowanych wartości oraz dodanie następującej reguły dla zmiennych:
    ρ ⊢ x ⇒v ρ(x), jeżeli x ∊ dom(ρ).
  5. Warto pozwolić programiście na definiowanie nazw dla skomplikowanych typów, jak opisano w podrozdziale 11.4 podręcznika.

Zadanie 2 (15p)

Zaimplementuj język funkcyjny z referencjami i automatycznym odśmiecaniem pamięci zgodnie z semantyką statyczną (typowaniem) i dynamiczną (SOS) podaną na wykładzie i omówioną w podręczniku. W tym celu możesz rozszerzyć system zaprogramowany w zadaniu 1 lub tylko pewien jego (pozwalający na interesujące testy) podzbiór. Pamiętaj o tym, że programy wejściowe nie mogą zawierać referencji, a co za tym idzie ich typowanie nie wymaga kontekstu typowania referencji.

Zadanie 3 (dla chętnych, 10p)

Zaproponuj (w postaci implementacji) system typów dla rachunku lambda z wyjątkami ([Pie02]:14), który podaje nie tylko informację o typie wyrażenia, ale i o nieobsłużonych wyjątkach, które dane wyrażenie może rzucić.