Programowanie funkcyjne/System typów

UNDER CONSTRUCTION

Składnia drobnego fragmentu Ocamla

<wyrażenie>    ::= <identyfikator> | <konstruktor> | 0 | 1 | ... 
                   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.

Typy i środowiska typujące

Przez typy proste bedziemy rozumieli napisy generowane przez następującą gramatykę:

<typ prosty>        ::= <zmienna typowa> | <typ prosty> \to <typ prosty> | 
                        <typ prosty>1 <typ prosty>n  <konstruktor typu>n
<konstruktor typu>  ::= int | bool | list | ...*...*... | ...
<zmienna typowa>    ::= \alpha | \beta | \gamma | ...
     

W momencie gdy zechcemy przypisywać typy obiektom polimorficznym, będą nam potrzebne schematy typów:

<schemat typu> ::= \forall_{\alpha_1, \dots, \alpha_n}.<typ prosty>\ |
                   <typ prosty>
     

Schemat typu ${\mathrm{\forall }}_{{\alpha }_1,\dots ,{\alpha }_n}.\tau$ możemy rozumieć jako opis zbioru wszystkich typów, jakie możemy uzyskać podstawiając w $\tau$ za ${\alpha }_1,\dots ,{\alpha }_n$ dowolne typy.

Środowisko typujące, to skończona funkcja (mapa) przypisująca identyfikatorom typy (proste, lub schematy, w zależności od potrzeby). 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⊢e:\tau$, co oznacza, że zakładając typowania ze środowiska $A$ możemy stwierdzić, że $e$ jest typu $\tau$.

Reguły typowania dla prostych typów

Bez polimorfizmu. Tylko monomorfizm. Let jest traktowany wyłącznie jak lukier syntaktyczny. Środowisko typujące używa wyłącznie typów prostych. \[ \frac{x \in dom(A)}{A \vdash x : A(x)} \] \[ \frac{A \vdash e_1:\tau_1    \dots    A\vdash e_n:\tau_n} {A \vdash (e_1, \dots, e_n) : \tau_1 * \cdots * \tau_n} \] \[ \frac{}{A \vdash () : unit} \] \[ \frac{A \vdash w:\mathtt{bool}    A\vdash e_1:\tau    A\vdash e_2:\tau} {A\vdash \mathtt{if}\ w\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2 : \tau} \] \[ \frac{A\vdash f : \tau_1 \to \tau_2    A\vdash e:\tau_1} {A\vdash f\ e : \tau_2} \] \[ \frac{A, x:\tau_1 \vdash e:\tau_2} {A \vdash (\mathtt{function}\ x \to e) : \tau_1 \to \tau_2} \] \[ \frac{A \vdash e_1:\tau_1    A, x:\tau_1 \vdash e_2:\tau_2} {A \vdash \mathtt{let}\ x = e_1\ \mathtt{in}\ e_2 : \tau_2} \] \[ \frac{A\vdash e:\tau}{A\vdash (e) : \tau} \] \begin{przyklad} Pokazać, że let id = (function x -> x) in id 42 : int.\end{przyklad} \begin{przyklad} Pokazać, że let id = (fun x -> x) in id id nie da się otypować (brak polimorfizmu). \end{przyklad}

Polimorfizm

Chcąc wyrazić, że jakieś wyrażenie (np.\ id w powyższym przykładzie) może przyjmować różne typy w różnych wystąpieniach, musimy użyć schematów typów. Taki schemat powinien opisywać wszystkie możliwe typy wartości polimorficznej.

\paragraph{Fakt:} Dla każdego wyrażenia istnieje (najbardziej ogólny) schemat typu, który obejmuje wszystkie typy, które można wyprowadzić dla tego wyrażenia.

Równocześnie powinniśmy być w stanie ukonkretniać ten typ na różne sposoby. \[ \frac{x \in dom(A), A(x) = \forall_{\overline{\alpha}}.\tau} {A \vdash x : \tau[\overline{\pi}/\overline{\alpha}]} \] \[ \frac{A \vdash e_1:\tau_1    A, x:\forall_{Free(\tau_1) \setminus Free(A)}.\tau_1 \vdash e_2:\tau_2} {A \vdash \mathtt{let}\ x = e_1\ \mathtt{in}\ e_2 : \tau_2} \]

\begin{przyklad} Pokazać, że let id = (fun x -> x) in id id jest typu $\alpha \to \alpha$. \end{przyklad}

Zauważmy, że mamy polimorficzną regułę dla let-a, ale nie mamy polimorficznej reguły dla $\lambda$-abstrakcji i aplikacji funkcji.

\begin{przyklad} Pokazać, że nie da się otypować (function id -> id id)(function x -> x).\end{przyklad}

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(\mathtt{fix}) = \forall_\alpha. (\alpha \to \alpha) \to \alpha \] Definicję rekurencyjną postaci: \[ \mathtt{let\ rec}\ f\ x = e_1\ \mathtt{in}\ e_2 \] zamieniamy na: \[ \mathtt{let}\ f = \mathtt{fix}(\mathtt{function}\ f \to \mathtt{function}\ x \to e_1) \ \mathtt{in}\ e_2 \] Zwróćmy uwagę, że wewnątrz definicji f funkcja ta niejest polimorficzna.

Wyjątki

\[ \frac{A \vdash e : \mathtt{exn}} {A \vdash \mathtt{raise}\ e : \tau} \] Uproszczona wersja --- nie wnikamy we wzorce. \[ \frac{A \vdash e_1:\tau    A,x:\mathtt{exn} \vdash e_2:\tau} {A \vdash \mathtt{try}\ e_1\ \mathtt{with}\ x \to e_2 : \tau} \]

Konstrukcje imperatywne i słabe zmienne typowe

Dla sekwencji instrukcji imperatywnych mamy regułę: \[ \frac{A \vdash e_1 : \tau_1    A \vdash e_2 : \tau} {A \vdash e_1;e_2 : \tau} \] Gdyz tak naprawdę ; możemy zdefiniować jako: let (;) x y = y;;

Gdzie jest problem?

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

Powinniśmy być w stanie pokazać, że $\mathtt{r}:{\mathrm{\forall }}_{\alpha }.(\alpha \to \alpha )\mathtt{r}\mathtt{e}\mathtt{f}$. Jeśli się zastanowimy jakiego typu są \texttt{:=} i !, to jedyne sensowne typy, to: \[ A \vdash \mathtt{:=} : \forall_\alpha.\alpha\ \mathtt{ref}\ \to \alpha \to\ \mathtt{unit} \] \[ A \vdash \mathtt{!} : \forall_\alpha.\alpha\ \mathtt{ref}\ \to \alpha \] Czyli, np.: \[ A, \mathtt{r}: \forall_\alpha.(\alpha \to \alpha)\ \mathtt{ref} \vdash \mathtt{(r := (function\ x \to x + 42))}:\mathtt{unit} \] \[ A, \mathtt{r}: \forall_\alpha.(\alpha \to \alpha)\ \mathtt{ref} \vdash \mathtt{!r}\ \mathtt{true} : \mathtt{bool} \] To jednak nie ma sensu!

Rozwiązaniem są tzw.\ słabe zmienne typowe, oznaczane jako $\mathrm{\_}\alpha$:

• • Słabe zmienne typowe nie są kwantyfikowane.

    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.

  (Top level.)

  • Uwaga

    Kompilator może nazywać różne słabe zmienne typowe

  tak samo.

  Trzeba sobie zdawać sprawę kiedy dwie zmienne typowe są

  różne.

  • Przy deklaracji let, typ stałej jest kwantyfikowany*;tylko wtedy, gdy wyrażenie definiujące stałą nie jest

  ekspansywne.**;Referencje i aplikacje są ekspansywne.

let r = ref (function x -> x);; val r : ('_a -> '_a) ref = {contents = <fun>}r := (function x -> 42);; 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 -> '_alet r = ref p;; val r : ('_a -> '_a) refp 42;; p: int -> int'r: (int -> int) ref   let r = ref id;; val r : ('_a -> '_a) reflet q = ref id;; val q : ('_a -> '_a) ref!r 42 r: (int -> int) ref'val q : ('_a -> '_a) ref   let r = ref id;; val r : ('_a -> '_a) reflet q = ref (!r);; val q : ('_a -> '_a) ref!r 42;; r: (int -> int) ref'q: (int -> int) ref   let f x =   let r = ref id   in (r := compose !r !r; !r x);; val f : 'a -> 'af 42;; = 42f true;; = true   let g =   let r = ref id   in (r := compose !r !r; !r);; val g : '_a -> '_ag 42;; = 42'g : int -> int   let f x = let r = ref x in (function y -> r := compose !r !r; !r y);;

[.....]

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

Jeśli zdefiniujemy procedurę, której typ zawiera słabe zmienne typowe, a chcemy, żeby miała silne, to możemy zastosować $\eta$-ekspansję, tzn.\ dodać formalny argument procedury. Jeżeli nie ma (imperatywnych) przeciwwskazań, to uzyskamy procedurę równoważną.