5109637318

Zadanie 4. Rozważmy system z poprzedniego zadania. Zauważ, że istnieją dokładnie dwa zamknięte termy typu Va.a —> a —> a. Typ ten może więc służyć do zakodowania typu bool. Zdefiniuj wartości true i false oraz komplet operacji logicznych. Zauważ, że wszystkie dają się wyrazić przy pomocy operatora if i że operator ten jest kodowany przez wyrażenie Xx.x (to nie przypadek). Pamiętając o liczebnikach Churcha zauważ dalej, że Va.(a: —* a) —» (a —> a) może reperezentować typ nat. Pokaż, że dowolny zamknięty term jest typu Vct.(a —* a) —* (o: —* a), wtedy i tylko wtedy, gdy jest liczebnikiem Churcha. Zdefiniuj podstawowe operacje arytmetyczne. Zauważ, że wszystkie dają się wyrazić przy pomocy iteratora iter, takiego, że iter nfc — fⁿ(c). Zauważ, że iter jest kodowany przez wyrażenie Xx.x (to nie przypadek). Zauważ dalej, że typ list(/?) = Va.(/3 —► a —* a) —> (a —» a) koduje listy typu (3. Zdefiniuj konstruktory i operacje działające na listach. Zauważ, że dają się one wyrazić przy pomocy iteratora f oldr i że f oldr jest kodowany przez wyrażenie Xx.x (to nie przypadek). Wywnioskuj z tych rozważań, że system F może służyć do zadania semantyki typów danych, takich, jak listy, krotki, liczby itp. Zakoduj kilka innych typów danych (unit, void, drzewa binarne itp.).

Zadanie 5. Pokaż, że polimorfizm parametryczny „kłóci się” ze skutkami ubocznymi. Rozważmy język

t    x | t\t2 | Xx.t | let x — ti in t2 \ n \ t\ + ti | True | False | ref t \ t\ : = t2 | ! t

t    a \ T\ —* T2 \ Int | Bool | Ref r

a ::= Va.r z regułami typowania

T, x : Ti h t: T2

T \- t: Ti —* t₂ T h s : T2

T h Xx.t : Ti —* T2 a = FV(ti) \ FV(r)

T, x : Vć?.r h x : rja/r']    T h ts : T2

r h ti : ri r, x : Va.n h t2 : T2

let x = t\ in t2 : T2 r h t\ : Int rbt₂ : Int

r h n : Int    T h ti + £2 ^: Iⁿt    T h True : Bool T h False : Bool

r b £ : r    r h ti : Ref r T \- t2'- t T h t : Ref a

r b ref t : Ref r

T\~ti : = t2 : t

Operator ref alokuje pamięć dla nowej zmiennej i inicjuje ją podaną wartością, : = jest operatorem przypisania, a ! — dereferencji. Np. program

let x = ref 1 in a: : = 2

alokuje pamięć dla komórki przechowującej dane typu Int, związuje adres tej komórki ze zmienną x typu Ref Int, inicjuje tę komórkę wartością 1, a następnie przypisuje jej wartość 2. Pokaż, że powyższy system jest sprzeczny i pozwala napisać program, który dodaje 1 do True. Wykorzystaj ten trik do zdefiniowania funkcji cast : a —> (3.

2