5109637320

Zadanie 9. Zauważ, że algebraiczne typy danych świetnie współgrają z polimorfizmem parametrycznym — deklaracja

data T a = C\ t{ ... t™¹ \ ... \ Ck ... r£^k

dodaje po prostu do składni termów stałe C\,...,Ck i wyrażenie case pozwalające dopasowywać wyrażenia do wzorców, do typów wyrażenie typowe T t\ ... t^, a do reguł typowania — reguły

T b Ci : t} -> ... -» 7f¹ — T a

Zdefiniuj składnię abstrakcyjną i napisz algorytm rekonstrukcji typów dla takiego języka. Zauważ, że musimy przyjąć następujące założenie:

(j FV(ti) ę 3,

3=1

inaczej system jest sprzeczny — pokaż, że jeśli dopuścilibyśmy deklarację data T = C a

to łatwo moglibyśmy napisać funkcję cast :: a -> b. (Tu jesteśmy o krok od wynalezienia typów egzystencjalnych).

Zadanie 10. Zauważ, że rekursja polimorficzna nie jest zjawiskiem egzotycznym lecz pojawia się w całkiem naturalnych problemach. Lista o bezpośrednim dostępie, to struktura danych udostępniająca operacje:

class RandomAccessList 1 where nil :: 1 a

cons :: a -> 1 a -> 1 a

head :: 1 a -> a

taił :: 1 a -> 1 a

lookup : : Int -> 1 a -> a

update :: a -> Int -> 1 a -> 1 a

Wszystkie operacje powinny się wykonywać w czasie logarytmicznym względem wielkości listy. Jedną z możliwych implementacji takiej listy jest

data Tree a = Node (Tree a, Tree a) | Leaf a type BinomialRAL a = [Tree a]

przy czym elementami listy [Tree a] są pełne drzewa binarne, a ich wysokości ściśle rosną. Powyższa reprezentacja jest nadmiarowa, gdyż wiele danych typu BinomialRAL jest nielegalnych. Aby system typów wykluczył nielegalne reprezentacje, powinniśmy tak zdefiniować typ Tree, by jedynymi danymi tego typu były drzewa pełne. Możemy to zrobić np. tak:

4