Programowanie funkcyjne/System typów

From Studia Informatyczne

Spis treści

Wstęp

W tym wykładzie zamiemy się systemem typów w Ocamlu oraz zasadom, na podstawie których kompilator wnioskuje o typach. Ograniczymy się przy tym do podstawowych konstrukcji języka i uprościmy trochę składnię. System typów w Ocamlu jest wariantem systemu Hindleya–Milnera.

<wyrażenie>    ::= <identyfikator> | <konstruktor> | 0 | 1 | ... 
                   ( <wyrażenie> { , <wyrażenie> }* ) |
                   if <wyrażenie> then <wyrażenie> else <wyrażenie> | 
                   <wyrażenie> <wyrażenie> |
                   function <identfikator> \to <wyrażenie> |
                   let <identyfikator> = <wyrażenie> in <wyrażenie> |
                   (<wyrażenie>)
<konstruktor> ::=  <Identyfikator> { <wyrażenie> }*      

Niektóre konstruktory i stałe mają specjalną składnię, np. konstruktor n-tki i operacje arytmetyczne. Gdy tylko nie będzie to budzić niejednoznaczności, a będzie to przydatne, będziemy traktowali konstruktory również jako nazwy procedur konstruujących wartości. Uprości to nasze rozważania, nie zmniejszając ich ogólności.

Typy i środowiska typujące

Będą nam potrzebne pojęcia typu prostego i schematu typów. Przez typy proste bedziemy rozumieli napisy postaci:

<typ prosty>           ::= <zmienna typowa>  |  ( <typ prosty> )  |  <typ prosty> -> <typ prosty> | 
                           <typ prosty> { * <typ prosty> }* |
                           <typ prosty>1 <typ prosty>2 ... <typ prosty>n  <konstruktor typu>n
<konstruktor typu>0    ::= int | bool | float | unit | ...
<konstruktor typu>1    ::= list | ...
                          \vdots
<zmienna typowa>       ::= <zmienna typowa silna>  |  <zmienna typowa słaba>
<zmienna typowa silna> ::= 'a | 'b | 'c | ...
<zmienna typowa słaba> ::= '_a | '_b | '_c | ...

Przyjmujemy, że konstruktory typów wiążą najsilniej, * słabiej, a -> najsłabiej. Przy tym -> jest lewostronnie łączne.

Przez schematy typów będziemy rozumieli napisy następującej postaci:

<schemat typu> ::= \underline{\forall} [ <zmienna typowa silna> { , <zmienna typowa silna> }* ] . <typ prosty>  |  
                   <typ prosty>

Typ prosty opisuje jeden typ, zależny od wartości ew. zawartych w nim zmiennych typowych. Schemat typów opisuje te typy, do których potrafi się przystosować wartość polimorficzna. Schemat typu \forall'a,'b,...,'g.t możemy rozumieć jako opis zbioru wszystkich tych typów, które możemy uzyskać podstawiając w t za 'a,'b,...,'g (równocześnie) dowolne typy. Silne zmienne typowe są też nazywane polimorficznymi, gdyż opisują to w jaki sposób wartości polimorficzne mogą być wielu typów.

Słabe zmienne typowe zostały wprowadzone ze względu na problemy na styku konstrukcji imperatywnych i polimorfizmu. Słaba zmienna typowa opisuje typ, który nie do końca jest znany. W szczególności, przy inkrementacyjnym trybie pracy z kompilatorem, słabe zmienne typowe mogą w trakcie interakcji być zastępowane konkretniejszymi typami. Tak więc nie opisują one polimorfizmu, lecz nie do końca rozpoznany monomorfizm. Nie mogą również być kwantyfikowane w schematach typów. Są one też nazywane monomorficznymi zmiennymi typowymi. Zajmiemy się dokładnie nimi dalej, gdy będziemy omawiać problemy na styku polimorfizmu i konstrukcji imperatywnych.

Będzie nam jeszcze potrzebne pojęcie środowiska typującego. Środowisko typujące, to skończona funkcja (mapa) przypisująca identyfikatorom typy (proste, lub schematy, w zależności od potrzeby). Przechowuje ono informacje potrzebne kompilatorowi do wyznaczania typów. Zakładamy istnienie takiego środowiska typującego wszystkie stałe i konstruktory wbudowane w język. Oczywiście typy tych stałych i konstruktorów muszą być zgodne z ich arnościami.

Niech A oznacza środowisko typujące. Przez A, x:\tau będziemy oznaczać środowisko identyczne z A, z tym wyjątkiem, że nazwie x przyporządkowuje typ \tau. Typowanie wyrażeń w programie będziemy oznaczali przez stwierdzenia postaci: A \vdash e : \tau, co można rozumieć następująco: "zakładając typowania ze środowiska A możemy stwierdzić, że e jest typu \tau.

Reguły typowania dla prostych typów

Sposób wnioskowania o typach możemy przedstawić w postaci reguł, podobnych do reguł dowodzenia w systemie dowodzenia. Nad poziomą kreską wymieniamy wszystkie przesłanki, a pod kreską wynikający z nich wniosek. W naszym przypadku, takim wnioskiem nie będzie formuła logiczna, ale stwierdzenie dotyczące typowania.

Oto podstawowe reguły opisujące typowanie wyrażeń. Ograniczają się one do typów monomorficznych. Nie obejmują one polimorfizmu, rekurencji i konstrukcji imperatywnych. Tak więc chwilowo pomijamy (słabe i silne) zmienne typowe.

Definicje lokalne let-in traktujemy tu jak lukier syntaktyczny, tzn. wyrażenia postaci let a = b in c rozwijamy do (function a -> c) b

Można wywnioskować wszystkie typy określone w środowisku.

\begin{array}{c} x \in dom(A)  \\\hline A \vdash x : A(x) \end{array}


Jeśli znane są typy współrzędnych n-ki, to jej typ jest odpowiednim typem produktowym.

\begin{array}{c} A \vdash e_1:\tau_1,\  \dots,\  A\vdash e_n:\tau_n \\\hline A \vdash (e_1, \dots, e_n) : \tau_1 * \cdots * \tau_n \end{array}


Pusta n-ka () jest zawsze typu unit.

\begin{array}{c} \\\hline A \vdash () : \mathtt{unit} \end{array}


W wyrażeniu warunkowym if-then-else pierwszy człon musi być typu bool, a dwa pozostałe muszą być tego samego typu. Taki też jest typ całego wyrażenia.

\begin{array}{c} A \vdash w:\texttt{bool},\  A\vdash e_1:\tau,\  A\vdash e_2:\tau \\\hline A\vdash \texttt{if}\ w\ \texttt{then}\ e_1\ \texttt{else}\ e_2 : \tau \end{array}


Jeśli znany jest typ procedury i typ argumentu pasuje do typu procedury, to wynik zastosowania procedury do argumentu ma taki typ, jak to wynika z typu procedury.

\begin{array}{c} A\vdash f : \tau_1 \to \tau_2,\  A\vdash e:\tau_1 \\\hline A\vdash f\ e : \tau_2} \end{array}


Jeżeli, przy założeniu, że parametr \lambda-abstrakcji jest typu \tau_1, można pokazać, że wynik \lambda-abstrakcji jest typu \tau_2, to sama \lambda-abstrakcja jest typu \tau_1 \to \tau_2.

\begin{array}{c} A, x:\tau_1 \vdash e:\tau_2 \\\hline A \vdash (\texttt{function}\ x \to e) : \tau_1 \to \tau_2 \end{array}


Jeżeli możemy wywnioskować jaki jest typ wartości definiowanej lokalnie, to typ tej wartości możemy umieścić w środowisku typującym i o typie wyrażenia let-in wnioskować na podstawie tak wzbogaconego środowiska i drugiego członu wyrażenia.

\begin{array}{c} A \vdash e_1:\tau_1 A, x:\tau_1 \vdash e_2:\tau_2 \\\hline A \vdash \texttt{let}\ x = e_1\ \texttt{in}\ e_2 : \tau_2 \end{array}

Nawiasy nie zmieniają typowania.

\begin{array}{c} A\vdash e:\tau \\\hline A\vdash (e) : \tau \end{array}


Przykład Typowanie

Oto wywód tego, że:

let id = (function x -> x) in id 42

jest typu int.

\def\rule#1#2{\begin{array}[b]{c}#1\\\hline#2\end{array}} \def\int{\mathtt{int}} \rule{   \rule{     \rule{     }{       42:\int, \texttt{x}:\int \vdash \texttt{x}:\int     }   }{     42:\int \vdash \texttt{(function x -> x)}:\int \to \int   } ~~   \rule{     \rule{     }{       42:\int, \texttt{id}:\int\to\int \vdash \texttt{id}:\int\to\int     }~~     \rule{     }{       42:\int, \texttt{id}:\int\to\int \vdash 42:\int     }   }{     42:\int, \texttt{id}:\int \to \int \vdash \texttt{id 42}:\int   } }{   42:\int \vdash \texttt{let id = (function x -> x) in id 42}:\int }

W powyższym typowaniu procedura id miała typ int -> int, choć mogłaby mieć dowolny typ pasujący do schematu \forall \alpha. \alpha \to \alpha. Jednak jakiego byśmy typu dla id nie przyjęli, to wszystkie wystąpienia tej procedury po prawej stronie in muszą mieć ten sam typ. Tak więc, np. dla wyrażenia:

let id = (fun x -> x) in id id

nie da się wyznaczyć żadnego typu. Żeby było to możliwe, potrzebne będzie wprowadzenie schematów typów i polimorfizmu.

Polimorfizm

Chcąc wyrazić, że jakieś wyrażenie (np. id w poprzednim przykładzie) może przyjmować różne typy w różnych wystąpieniach, musimy użyć schematów typów. Wprowadzamy więc schematy typów i silne zmienne typowe. Pomijamy jednak nadal kwestię słabych zmiennych typowych. Schemat typu postaci \forall'a,'b,...,'g.t reprezentuje zbiór wszystkich tych typów prostych, które możemy uzyskać podstawiając za 'a,'b,...,'g (równocześnie) w t dowolne typy proste.

Taki schemat powinien opisywać wszystkie możliwe typy wartości polimorficznej i faktycznie jest to możliwe. Równocześnie powinniśmy być w stanie ukonkretniać taki schemat typu na różne sposoby.

Fakt

Dla każdego wyrażenia istnieje (najbardziej ogólny) schemat typu, obejmujący wszystkie typy, które można wyprowadzić dla tego wyrażenia (przy użyciu reguł pokazanych powyżej).

Potrzebujemy dwóch reguł, które by rozszerzyły dotychczasowe reguły o polimorfizm. Jednej, która by wprowadzała schematy typów do środowisk typujących i jednej, która by je interpretowała.

Przez Free(\tau) oznaczamy ziór zmiennych typowych występujących w \tau i nie związanych pod kwantyfikatorem, a przez Free(A) oznaczamy ziór zmiennych typowych, które są wolne w którymkolwiek typie przypisywanym przez A. Ponadto, przez \overline{\alpha} oznaczamy tu wektor silnych zmiennych typowych, przez \overline{\pi} oznaczamy tu (tej samej długości) wektor typów prostych, a przez \tau[\overline{\pi}/\overline{\alpha}] oznaczamy typ powstały przez równoczesne zastąpienie zmiennych z \overline{\alpha} przez odpowiadające im typy z \overline{\pi}.

\begin{array}{c}   A(x) = \forall_{\overline{\alpha}}.\tau   \\\hline   A \vdash x : \tau[\overline{\pi}/\overline{\alpha}] \end{array}

\begin{array}{c}   A \vdash e_1:\tau_1,\ A, x:\forall_{Free(\tau_1) \setminus Free(A)}.\tau_1 \vdash e_2:\tau_2   \\\hline   A \vdash \texttt{let}\ x = e_1\ \texttt{in}\ e_2 : \tau_2 \end{array}

Pierwsza reguła mówi, że zmienne kwantyfikowane możemy zastąpić dowolnymi typami, i to za każdym razem innymi. Druga reguła mówi, że jeżeli potrafimy wyprowadzić dla wartości symbolu definiowanego lokalnie typ zawierający wolne zmienne typowe i to niezależne od ew. wolnych zmiennych typowych występujących w środowisku, to możemy je kwantyfikować.


Przykład Polimorfizm

Poniższe typowanie pokazuje, że wyrażenie:

let id = (function x -> x) in id id

jest typu \alpha \to \alpha.

\def\rule#1#2{\begin{array}[b]{c}#1\\\hline#2\end{array}} \rule{   \rule{     \rule{}{A, \texttt{x}:\beta \vdash \texttt{x}:\beta}   }{     A\vdash \texttt{(function x -> x)}: \beta\to\beta   }~~   \rule{     \rule{}{       A, \texttt{id}:\forall \beta.\beta\to\beta \vdash \texttt{id}: (\alpha\to\alpha) \to (\alpha\to\alpha)     }~~     \rule{}{       A, \texttt{id}:\forall \beta.\beta\to\beta \vdash \texttt{id}: \alpha\to\alpha     }   }{     A, \texttt{id}:\forall \beta.\beta\to\beta \vdash \texttt{id id}:\alpha\to\alpha   } }{   A\vdash \texttt{let id = (function x -> x) in id id}:\alpha \to \alpha }

Zauważmy, że mamy polimorficzną regułę dla wyrażeń let-in, ale nie mamy polimorficznej reguły dla \lambda-abstrakcji i aplikacji funkcji. Tak więc wyrażenie let-in nie jest dokładnie lukrem syntaktycznym pokrywającym \lambda-abstrakcję. Weźmy wyrażenie:

(function id -> id id)(function x -> x)

Nie da się wyznaczyć typu dla tego wyrażenia typu. Dwie reguły podane w tym punkcie nie mają zastosowania, gdyż nie jest to wyrażenie let-in.

Rekurencja

Jak możemy wnioskować o typie procedur rekurencyjnych? Sięgnijmy po technikę podobną do prezentowanej wcześniej. Definicję rekurencyjną możemy wyrazić jako punkt stały. Załóżmy, że środowisko typujące zawiera operator punktu stałego:

A(\texttt{fix}) = \forall_\alpha. (\alpha \to \alpha) \to \alpha

Definicję rekurencyjną postaci:

\texttt{let\ rec}\ f\ x = e_1\ \texttt{in}\ e_2

zamieniamy na:

\texttt{let}\ f = \texttt{fix}(\texttt{function}\ f \to \texttt{function}\ x \to e_1)\ \texttt{in}\ e_2

Zwróćmy uwagę, że wewnątrz definicji f funkcja ta nie jest polimorficzna. Może się taka stać dopiero po prawej stronie in.

Wyjątki

Podniesienie wyjątku przerywa obliczenie, bez względu na to jakiego typu wartość jest obliczana.

\begin{array}{c} A \vdash e : \texttt{exn} \\\hline A \vdash \texttt{raise}\ e : \tau \end{array}

Przechwytując wyjątek powinniśmy zapewnić wartość tego samego typu, co gdyby żaden wyjątek nie był podniesiony.

\begin{array}{c} A \vdash e_1:\tau A,x:\texttt{exn} \vdash e_2:\tau \\\hline A \vdash \texttt{try}\ e_1\ \texttt{with}\ x \to e_2 : \tau \end{array}

Konstrukcje imperatywne i słabe zmienne typowe

Dla sekwencji instrukcji imperatywnych mamy regułę:

\begin{array}{c} A \vdash e_1 : \tau_1 A \vdash e_2 : \tau \\\hline A \vdash e_1;e_2 : \tau \end{array}

Gdyz tak naprawdę ; możemy zdefiniować jako:

let (;) x y = y;;

Gdzie jest problem z imperatywnością i polimorfizmem? Prześledźmy następujący przykład.

let r = ref (function x -> x);;

Powinniśmy być w stanie pokazać, że:

\texttt{r}: \forall_\alpha.(\alpha \to \alpha)\ \texttt{ref}

Jeśli się zastanowimy jakiego typu są := i !, to jedyne sensowne typy, to:

A \vdash \texttt{:=} : \forall_\alpha.\alpha\ \texttt{ref}\ \to \alpha \to\ \texttt{unit}

A \vdash \texttt{!} : \forall_\alpha.\alpha\ \texttt{ref}\ \to \alpha

Czyli, np.:

A, \texttt{r}: \forall_\alpha.(\alpha \to \alpha)\ \texttt{ref} \vdash  (r := (\texttt{function}\ x \to x + 42)) : \texttt{unit}

A, \texttt{r}: \forall_\alpha.(\alpha \to \alpha)\ \texttt{ref} \vdash \texttt{!r}\ \texttt{true} : \texttt{bool}

To jednak nie ma sensu!

Rozwiązaniem są tzw. słabe zmienne typowe, oznaczane jako '_a, '_b, .... Słabe zmienne typowe nie są kwantyfikowane, a silne tak. Słabe zmienne typowe są monomorficzne. Reprezentują one jeden typ, a nie wiele, ale jeszcze nie do końca poznany. Za słabe zmienne typowe (w trakcie rekonstrukcji typów) można podstawić typy proste zawierające tylko słabe zmienne typowe. Każda próba podstawienia za słabą zmienną typową jakiegoś typu powoduje, że na stałe zostaje ona zastąpiona tym typem.

Uwaga: Kompilator może nazywać różne słabe zmienne typowe tak samo. Wynika to stąd, że wypisując typy stara się używać jak najmniej nazw zmiennych typowych. Przez to, pewne zależności między zmiennymi w typach różnych wartości przestają być widoczne. Trzeba sobie zdawać sprawę kiedy dwie słabe zmienne typowe są różne.

W deklaracjach let, typ stałej jest kwantyfikowany tylko wtedy, gdy wyrażenie definiujące stałą nie jest ekspansywne. Jeśli jest ono ekspansywne, to wszystkie silne zmienne typowe w typie są zamieniane na słabe. Kryterium ekspansywności jest czysto składniowe. Nieekspansywne są te wyrażenia, które są zbyt proste, żeby mogły utworzyć np. referencje. Nieekspansywne są:

  • stałe i identyfikatory,
  • n-ki, których współrzędne nie są ekspansywne,
  • wartości zbudowane za pomocą konstruktorów, o ile ich argumenty nie są ekspansywne,
  • \lambda-abstrakcje (oraz definicje procedur nazwanych z jawnie podanymi argumentami).
Wartości proceduralne sa nieekspansywne, gdyż ich treść jest obliczana dopiero po podaniu argumentów. Wszystkie pozostałe wyrażenia są ekspansywne. W szczególności ekspansywne są:
  • referencje i
  • aplikacje procedur do argumentów.

let r = ref (function x -> x);;
val r : ('_a -> '_a) ref = {contents = <fun>}

r := (function x -> 42);;
val r : (int -> int) ref

let id = (function x -> x);;
val id : 'a -> 'a = <fun>

let idd = id id;;
val idd : '_a -> '_a = <fun>

let idd x = id id x;;
val idd : 'a -> 'a = <fun>

let p = id id;;
val p : '_a -> '_a

let r = ref p;;
val r : ('_a -> '_a) ref

p 42;;
val p: int -> int
val r: (int -> int) ref

let r = ref id;;
val r : ('_a -> '_a) ref

let q = ref id;;
val q : ('_a -> '_a) ref

!r 42;;
val r: (int -> int) ref
val q : ('_a -> '_a) ref

let r = ref id;;
val r : ('_a -> '_a) ref

let q = ref (!r);;
val q : ('_a -> '_a) ref

!r 42;;
val r: (int -> int) ref
val q: (int -> int) ref

let f x = 
  let r = ref id 
  in (r := compose !r !r; !r x);;
val f : 'a -> 'a

f 42;;  
- : int = 42

f true;; 
- : bool = true

let g = 
  let r = ref id 
  in (r := compose !r !r; !r);;
val g : '_a -> '_a

g 42;; 
- : int = 42
val g : int -> int

let f x = 
  let r = ref x 
  in (function y -> r := compose !r !r; !r y);;   
val f : ('a -> 'a) -> 'a -> 'a = <fun>

let f x = 
  let r = ref x 
  in (function y -> r := y; !r);;
val f : 'a -> 'a -> 'a        

Niestety reguły wnioskowania o typach narzucone przez konstrukcje imperatywne dotykają również programów czysto funkcyjnych. Podział na wyrażenia ekspansywne i nie, nie zależy od tego, czy faktycznie zawierają one konstrukcje imperatywne, lecz jest czysto składniowy. Można więc napisać czysto funkcyjne wyrażenie, które będzie ekspansywne i w jego typie będą tylko słabe zmienne typowe.

Zwykle ma to miejsce w przypadku zastosowania proceudry wyższego rzędu, której wynikiem jest procedura polimorficzna. W takim przypadku należy zastosować tzw. \eta-konwersję, tzn.\ dodać formalny argument procedury (po obu stronach). Jeżeli nie ma (imperatywnych) przeciwwskazań, to uzyskamy procedurę równoważną, ale zdefiniowaną przy użyciu wyrażenia, które nie jest ekspansywne. Przywróci to silne zmienne w typie wyrażenia.

Ćwiczenia

Ćwiczenia