5109637317

Programowanie

Lista zadań nr 15

Na ćwiczenia 11, 19 i 23 czerwca 2008

Zadanie 1. Pokaż, że w systemie z polimorfizmem parametrycznym można napisać program P_n rozmiaru 0(n), którego typ ma rozmiar 2²ⁿ⁽ⁿ⁾.

Pokaż, że typ wyrażenia rozmiaru n w systemie z polimorfizmem parametrycznym

o2°(ⁿ>

ma rozmiar 2

Zadanie 2. Wyznacz typ główny er i napisz dowód sądu typowego w polimorficznym systemie typów Damasa-Milnera:

h let / = \x.x in // end : a

Zadanie 3. Rozważmy system, w którym konstrukcja Va.cr nie jest schematem typu, lecz zwykłym typem, tj. język, którego abstrakcyjna składnia jest następująca:

e    x\ e\e2 \ \x.e

a ::= a \ <J\ —»<T2 | Va.<7

i w którym przyjęto następujące reguły typowania:

Y,x \ a \~ x \ a

T b e\ : er —» t r h e2 : ff r,a::crhe:r r h eie2 : r    Th \x.e : a t

a i FV(r)

r h e : a

The: Va.<7

The: Vq.ct The: a[a/r]

Jest to tak zwany rachunek typów drugiego rzędu lub system F. Pokaż, że w tym systemie wyrażenie \x.xx posiada typ, podczas gdy w języku z tzw. płytkim polimorfizmem, tj. w systemie Damasa-Milnera — nie. Wskaż przykład termu, który nie posiada typu w nowym systemie. Pokaż, że każdy term, który posiada typ w prostym systemie typów posiada go i w nowym. Pokaż, że jeżeli do składni wyrażeń dodać let i przyjąć w systemie F tłumaczenie Landina, to każdy let-term typowalny w ML-u ma też typ w systemie F z tłumaczeniem Landina (zatem let jest jedynie cukrem syntaktycznym w monomorficznym systemie typów i w systemie F, lecz ma kluczowe znaczenie dla polimorfizmu w ML-u).

1