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> ::= ${\mathrm{\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⊢x:A(x)}$

$\frac{A⊢e_1:{\tau }_1\dots A⊢e_n:{\tau }_n}{A⊢(e_1,\dots ,e_n):{\tau }_1*\cdots *{\tau }_n}$

$\frac{}{A⊢():unit}$

$\frac{A⊢w:\text{<mrow data-mjx-texclass="ORD">bool</mrow>}A⊢e_1:\tau A⊢e_2:\tau }{A⊢\text{<mrow data-mjx-texclass="ORD">if</mrow>}w\text{<mrow data-mjx-texclass="ORD">then</mrow>}{e}_1\text{<mrow data-mjx-texclass="ORD">else</mrow>}{e}_2:\tau }$

$\frac{A⊢f:{\tau }_1\to {\tau }_{2}A⊢e:{\tau }_1}{A⊢fe:{\tau }_2}$

$\frac{A,x:{\tau }_1⊢e:{\tau }_2}{A⊢(\text{<mrow data-mjx-texclass="ORD">function</mrow>}x\to e):{\tau }_1\to {\tau }_2}$

$\frac{A⊢e_1:{\tau }_{1}A,x:{\tau }_1⊢e_2:{\tau }_2}{A⊢\text{<mrow data-mjx-texclass="ORD">let</mrow>}x=e_1\text{<mrow data-mjx-texclass="ORD">in</mrow>}{e}_2:{\tau }_2}$

$\frac{A⊢e:\tau }{A⊢(e):\tau }$

Przykład

Pokazać, że:

let id = (function x -> x) in id 42 : int.

Przykład

Pokazać, że:

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

nie da się otypować (brak polimorfizmu).

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.

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)={\mathrm{\forall }}_{\bar{\alpha }}.\tau }{A⊢x:\tau [\bar{\pi }/\bar{\alpha }]}$

$\frac{A⊢e_1:{\tau }_{1}A,x:{\mathrm{\forall }}_{Free({\tau }_1)\setminus Free(A)}.{\tau }_1⊢e_2:{\tau }_2}{A⊢\mathtt{l}\mathtt{e}\mathtt{t}x=e_1\mathtt{i}\mathtt{n}{e}_2:{\tau }_2}$

Przykład

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

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

Przykład

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ą.

Laboratoria i ćwiczenia

Laboratoria i ćwiczenia do wykładu