Programowanie funkcyjne/System typów

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

<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 | ...
                          $⋮$
<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> ::= $\underset{\_}{\mathrm{\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. Wymagamy przy tym, aby wszystkie silne zmienne typowe były związane pod kwantyfikatorem. Schemat typu $\mathrm{\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⊢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 regół 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.

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

$\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⊢\text{<mrow data-mjx-texclass="ORD">let</mrow>}x=e_1\text{<mrow data-mjx-texclass="ORD">in</mrow>}{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(\text{<mrow data-mjx-texclass="ORD">fix</mrow>})={\mathrm{\forall }}_{\alpha }.(\alpha \to \alpha )\to \alpha$

Definicję rekurencyjną postaci:

zamieniamy na:

$\text{<mrow data-mjx-texclass="ORD">let</mrow>}f=\text{<mrow data-mjx-texclass="ORD">fix</mrow>}(\text{<mrow data-mjx-texclass="ORD">function</mrow>}f\to \text{<mrow data-mjx-texclass="ORD">function</mrow>}x\to e_1)\text{<mrow data-mjx-texclass="ORD">in</mrow>}{e}_2$

Zwróćmy uwagę, że wewnątrz definicji f funkcja ta niejest polimorficzna.

Wyjątki

$\frac{A⊢e:\text{<mrow data-mjx-texclass="ORD">exn</mrow>}}{A⊢\text{<mrow data-mjx-texclass="ORD">raise</mrow>}e:\tau }$

Uproszczona wersja --- nie wnikamy we wzorce.

$\frac{A⊢e_1:\tau A,x:\text{<mrow data-mjx-texclass="ORD">exn</mrow>}⊢e_2:\tau }{A⊢\text{<mrow data-mjx-texclass="ORD">try</mrow>}{e}_1\text{<mrow data-mjx-texclass="ORD">with</mrow>}x\to e_2:\tau }$

Konstrukcje imperatywne i słabe zmienne typowe

Dla sekwencji instrukcji imperatywnych mamy regułę:

$\frac{A⊢e_1:{\tau }_{1}A⊢e_2:\tau }{A⊢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:

$\text{r}:{\mathrm{\forall }}_{\alpha }.(\alpha \to \alpha )\text{<mrow data-mjx-texclass="ORD">ref</mrow>}$

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

$A⊢\text{<mrow data-mjx-texclass="ORD"><mo stretchy="false">:</mo><mo stretchy="false">=</mo></mrow>}:{\mathrm{\forall }}_{\alpha }.\alpha \text{<mrow data-mjx-texclass="ORD">ref</mrow>}\to \alpha \to \text{<mrow data-mjx-texclass="ORD">unit</mrow>}$

$A⊢\text{<mo stretchy="false">!</mo>}:{\mathrm{\forall }}_{\alpha }.\alpha \text{<mrow data-mjx-texclass="ORD">ref</mrow>}\to \alpha$

Czyli, np.:

$A,\text{r}:{\mathrm{\forall }}_{\alpha }.(\alpha \to \alpha )\text{<mrow data-mjx-texclass="ORD">ref</mrow>}⊢(r:=(\text{<mrow data-mjx-texclass="ORD">function</mrow>}x\to x+42))$

$A,\text{r}:{\mathrm{\forall }}_{\alpha }.(\alpha \to \alpha )\text{<mrow data-mjx-texclass="ORD">ref</mrow>}⊢\text{<mrow data-mjx-texclass="ORD"><mo stretchy="false">!</mo>r</mrow>}\text{<mrow data-mjx-texclass="ORD">true</mrow>}:\text{<mrow data-mjx-texclass="ORD">bool</mrow>}$

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 -> '_a
let r = ref p;;
val r : ('_a -> '_a) ref
p 42;;
p: int -> int'r: (int -> int) ref
  
let r = ref id;;
val r : ('_a -> '_a) ref
let 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) ref
let 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 -> 'a
f 42;;  = 42
f true;; = true
  
let g = 
  let r = ref id 
  in (r := compose !r !r; !r);;
val g : '_a -> '_a
g 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