Odvodenie typu

Typová rekonštrukcia

V rámci predchádzajúcich prednášok sme venovali algoritmu typovej kontroly, ktorá vyžadovala explicitné typové anotácie. Pri $\lambda$-abstrakcii je nutné explicitne uviesť typ jej argumentu, ako aj typ celého termu. V dnešnej prednáške sa budeme venovať algoritmu typovej rekonštrukcie (odvodenie typu), vďaka ktorému je možné vynechať niektoré resp. aj všetky typové anotácie.

Odvodenie typu

Odvodenie typu je proces určenia vhodných typov výrazu na základe toho ako sú použité. Napríklad môžeme jednoducho odvodiť, že vo výraze $$\lambda f. f~3,$$ $3$ - argument funkcie je konštanta typu $Nat$ a $f$ je funkcia (nie kvôli svojmu názvu $f$, ale kvôli tomu, že je aplikovaná na nejaký argument). Na základe uvedených podmienok (obmedzení) je možné odvodiť: $$f:Nat \rightarrow X$$ a celý výraz je typu: $$\lambda f. f~3:(Nat \rightarrow X) \rightarrow X.$$

$X$ reprezentuje typovú premennú. Keďže funkcia očakáva na vstupe funkciu, ktorá má parameter typu $Nat$, avšak nevieme aký bude výstup. Pojem typová premenná je vysvetlený nižšie.

Pre overenie korektnosti nášho uvažovania prepíšeme daný term do jazyka OCaml, prostredníctvom ktorého sa následne pokúsime odvodiť typ.

utop # fun f -> f 3;; 
- : (int -> 'a) -> 'a = <fun>

Upravíme náš program a znova sa pokúsime odvodiť typ:

utop # fun f -> f (f 3);; 
- : (int -> int) -> int = <fun>

utop # fun f -> f (f "ahoj");; 
- : (string -> string) -> string = <fun>

utop # fun f -> f (f 3, f 4);; 
Error: This expression has type int but an expression was expected of type
         'a * 'b

Pozrime sa bližšie na výstup z interpretera jazyka OCaml. Pouvažujte, ako v prvom prípade OCaml vedel, že výstup funkcie $f$ je typu $Int$. Pretože vo výraze $f~(f~3)$ je vnútorné $f$ aplikované na argument typu $Int$ a tento výstup je vstupom pre vonkajšie $f$.

Definícia:
Ak je term správne typovaný potom jeho typ môže byť odvodený.

utop # 
let sq=fun z -> z*z in
   fun f -> fun x -> fun y -> 
     if f x y 
     then (f (sq x) y)
     else (f x (f x y));;
- : (int -> bool -> bool) -> int -> bool -> bool = <fun>

Obsah

1. Typová premenná.
2. Typová substitúcia.
3. Odvodenie typu na základe obmedzení (z ang. constraint-based typing).
   1. Obmedzenie.
   2. Typová relácia s obmedzeniami a príslušné typové pravidlá.
   3. Množina obmedzení $C$.
4. Unifikačný algoritmus - riešenie množiny obmedzení.
5. Najvšeobecnejší unifikátor (z ang. most general unifier).
6. Najvšeobecnejší typ (z ang. principle type).

Postup

Majme dané ľubovoľný term $t$ a kontext $\Gamma$.

1. Prostredníctvom typových pravidiel pre novú typovú reláciu, odvodíme typ $S$ a množinu obmedzení $C$ pre term $t$ a kontext $\Gamma$.
2. Nájdeme riešenie množiny obmedzení $C$, prostredníctvom algoritmu unifikácie.
   1. Vstup: množina obmedzení.
   2. Výstup: najvšeobecnejší unifikátor - substitúcia $\sigma$.
3. Aplikujeme substitúciu $\sigma$ na odvodený typ $S$ a získame najvšeobecnejší typ $T$.

Typové premenné

V jednoducho typovanom $\lambda$-kalkule je definovaná množina základných typov ako napr. Bool, Nat, Unit, ktorá zároveň obsahuje aj neinterpretované typy $T_1,T_2...$. Neinterpretované typy je možné definovať ako typové premenné.

Množina $\chi$ obsahujúca typové premenné $X,Y,Z$ je definovaná nasledovne: $$\chi=\{X,Y,Z,...\}.$$

• Z typových premenných a typových konštruktorov je možné vytvárať typové výrazy.
• Substitúcia typovej premennej konkrétnym typom vytvára typovú inštanciu.
• Množinu všetkých typov označíme ako $Types$.

• Množina $Types=\{T_1,T_2,...,Bool, Nat, Unit, ...\}$ obsahuje konkrétne typy jazyka.
• Množina $\chi=\{X,Y,Z,...\}$ obsahuje typové premenné.

Typová substitúcia

Neformálne, operáciu typovej substitúcie (ďalej len substitúcie, kde je z kontextu jasné, že sa jedná o typovú substitúciu) je možné chápať ako dosadenie konkrétneho typu za typovú premennú.

Špecifikácia zobrazenia substitúcie

Formálne substitúcia $\sigma$ je konečné zobrazenie špecifikované nasledovne: $$\sigma: \chi \rightarrow Types,$$ z typových premenných do typov. To znamená, aplikáciou zobrazenia $\sigma$ na určitý typový výraz získame konkrétny typ - inštanciu typového výrazu.

Definícia zobrazenia substitúcie

Nech $\sigma$ je substitúcia, $X$ je typová premenná, $T$ je typ. Potom konečné zobrazenie typovej substitúcie je možné definovať nasledovne: $$ \begin{array}{lcl} \sigma(X) & = & \begin{cases} T \quad ak \quad (X \mapsto T) \in \sigma \\ X \quad ak \quad X \notin dom(\sigma) \\ \end{cases} \\ \sigma(Nat) & = & Nat \\ \sigma(Bool) & = & Bool \\ \sigma(T_1 \rightarrow T_2) & = & \sigma T_1 \rightarrow \sigma T_2 \end{array} $$

Substitúcia aplikovaná na kontext: $$ \begin{array}{lcl} \sigma(x_1:T_1,... ,x_n:T_n) & = & x_1:\sigma T_1,... , \sigma x_n: \sigma T_n. \end{array} $$

Analogicky v prípade aplikácie substitúcie na term $t$, je substitúcia aplikovaná na všetky typy, ktoré sa nachádzajú v typových anotáciách $t$.

Nech $\sigma, \gamma$ sú substitúcie, potom kompozícia typových substitúcií $\sigma \circ \gamma$ je definovaná nasledovne:

$$ \sigma \circ \gamma = \left[ \begin{array}{ll} X \mapsto \sigma(T)\quad & \text{pre každé } (X \mapsto T) \in \gamma\\ X \mapsto T \quad & \text{pre každé } (X \mapsto T) \in \sigma \text{ také, že } X \notin dom(\gamma)\\ \end{array} \right] $$

Odvodenie typu na základe obmedzení

V tejto kapitole si predstavíme algoritmus, ktorý pre ľubovoľný term $t$ a kontext $\Gamma$ vypočíta množinu obmedzení - rovností medzi typovými výrazmi (prípadne aj typovými premennými), ktorá musí byť splnená v akékoľvek riešení pre ($\Gamma, t$).

Definícia: Množina obmedzení $C$ je množina rovností v tvare: $$C=\{S_i=T_i^{i\in 1...n}\},$$ kde $S_i, T_i$ sú ľubovoľné typy.

Obmedzenie má tvar $T_1 = T_2$, pre akékoľvek $T_1, T_2$.

Definícia: Unifikácia rovnosti $S$ a $T$ je taká substitúcia $\sigma$, že $$\sigma S = \sigma T.$$ Hovoríme, že substitúcia $\sigma$ unifikuje (spĺňa) množinu obmedzení $C$, ak unifikuje každú rovnosť v $C$.

Definícia: Typová relácia s obmedzeniami: $$\Gamma \vdash t:T~|~C,$$ ktorú je možné prečítať ako "term $t$ odvodzuje typ $T$ v prostredí $\Gamma$ a generuje množinu obmedzení $C$".

Ak uvažujeme o tejto relácii ako o funkcii, potom:

• dvojbodka $:$ v strede oddeľuje vstup od výstupu,
• vstup: $\Gamma, t$, chceme zistiť či term $t$ v prostredí $\Gamma$ má typ,
• výstup: typ $T$ a množina obmedzení $C$, ktorú musí typ $T$ spĺňať aby term $t$ v prostredí $\Gamma$ bol správne typovaný.

Jednoducho typovaný $\lambda$-kalkul

Pripomeňme si fragment nášho jazyka jednoducho typovaného $\lambda$-kalkulu s NBL, pre ktorý následne zadefinujeme typové pravidlá pre typovú reláciu s obmedzeniami: $$ \begin{array}{lcl} t & ::= & x ~|~ \lambda x :T.t ~|~ \lambda x.t ~|~t~t ~|~ 0 ~|~ true ~|~ false ~|~ succ~t ~|~\\ & & ~|~ pred~t ~|~ iszero~t ~|~~if~t~then~t~else~t~ \\ v & ::= & \lambda x:T.t ~|~ \lambda x.t ~|~ true ~|~ false ~|~ nv\\ nv & ::= & 0 ~|~ succ~nv\\ T & ::= & A ~|~ T \rightarrow T ~|~ X\\ A & ::= & Nat ~|~ Bool \end{array} $$

Typové pravidlá pre typovú reláciu s obmedzeniami

Pravidlá pre konštanty sú axiómy a pravidlo pre premennú kontroluje jej výskyt v typovom kontexte. Tieto pravidla negenerujú obmedzenia.

Pravidlá pre abstrakciu sú dve a to pre prípad kde je uvedená typová anotácia parametra abstrakcie (CT-Abs) alebo nie je (CT-AbsInf). V druhom prípade (CT-AbsInf) je potrebné zaviesť novú typovú premennú $X$ (niekedy v ang. nazývaná fresh variable).

Pravidlo pre aplikáciu vyžaduje zavedenie novej typovej premennej $X$ a vytvára obmedzenie $C$, ktoré je zjednotením obmedzení oboch predpokladov a rozširuje množinu o rovnosť $T_1=T_2\rightarrow X$, pričom $X$ musí byť nová typová premenná.

Pravidlá pre termy If, Succ, Pred, Iszero vytvárajú nové obmedzenie $C$ nasledovne:

• V prípade pravidla pre $CT-If$ nové obmedzenie $C$ pozostáva zo zjednotení obmedzení zo všetkých predpokladov pravidla a rozširuje ho o rovnosti $T_1=Bool, T_2=T_3$.
• V prípade pravidiel $CT-Succ, CT-Pred, CT-Iszero$ nové obmedzenie pozostáva zo zjednotenia obmedzenia z predpokladu pravidla o rovnosť $T=Nat$.

Definícia:
Nech je daný nasledujúci sekvent: $$\Gamma \vdash t:S ~|~ C.$$ Potom riešenie štvorice $$(\Gamma,t,S,C)$$ je taká dvojica $$(\sigma, T),$$ že $\sigma$ spĺňa $C$ a zároveň: $$\sigma S = T.$$

utop # fun x -> if x then 1 else 0;;
- : bool -> int = <fun>

Najvšeobecnejší unifikátor a najvšeobecnejší typ

Majme danú identickú funkciu: $$id=\lambda x:T.x:T \rightarrow T.$$ Tento term je správne typovaný pre ľubovoľný typ $T$. Napríklad: $$\lambda x:Nat.x:Nat \rightarrow Nat,$$ pričom $\sigma=[T\mapsto Nat]$. Aj napriek tomu, že táto funkcia sa stále správa rovnako, v prípade potreby aplikácie tejto funkcie na argument iného typu, je nutné napísať vlastnú funkciu s príslušným typom: $$ \begin{array}{l} \lambda x:Bool.x:Bool \rightarrow Bool\\ \lambda x:Nat\rightarrow Bool.x:(Nat\rightarrow Bool) \rightarrow (Nat\rightarrow Bool)\\ ..., \end{array} $$ čo v konečnom dôsledku vytvára nekonečné množstvo unifikátorov: $$ \begin{array}{l} \sigma=[T\mapsto Bool]\\ \sigma=[T\mapsto Nat\rightarrow Bool]\\ .... \end{array} $$

Takéto riešenie z hľadiska softvérového inžinierstva nie je žiadúce. Tento problém je možné vyriešiť zavedením polymorfizmu, kde namiesto konkrétneho typu sa v typových anotáciách budú môcť vyskytovať typové premenné a typová rekonštrukcia odvodí konkrétny typ podľa potreby (napr. podľa typu argumentu).

Demonštrácia uvedeného v jazyku OCaml:

utop # let id : int -> int = fun x -> x;;
val id : int -> int = <fun>

utop # id 4;;
- : int = 4

utop # id "ahoj";;
Error: This expression has type string but an expression was expected of type
         int

utop # let id_poly  = fun x -> x;;
val id_poly : 'a -> 'a = <fun>

utop # id_poly 4;;
- : int = 4

utop # id_poly "ahoj";;
- : string = "ahoj"

Najvšeobecnejší unifikátor

Z vyššie uvedeného vyplýva, že našim cieľom nie len nájsť ľubovoľné riešenie ($\sigma$, $T$) aby platilo $\sigma S = T$, ale hľadáme najvšeobecnejšie riešenie (unifikátor) $\sigma_{mgu}$. Zároveň platí, že ak existuje také $\sigma$, že $\sigma S = T$, potom existuje aj najvšeobecnejší unifikátor.

Definícia: Unifikátor $\sigma$ je všeobecnejší (more general) ako unifikátor $\sigma_2$, ak existuje taký unifikátor $\sigma_1$, že platí: $$\sigma_1 \circ \sigma = \sigma_2.$$

Definícia: Najvšeobecnejší unifikátor (z ang. Most General Unifier (MGU)) dvoch typov $S,T$ je taký unifikátor $\sigma$, že platí:

• $\sigma$ je unifikátor typov ($S,T$),
• $\sigma$ je všeobecnejší ako ľubovoľný iný unifikátor ($S,T$).

Najvšeobecnejší typ

Ako je možné vidieť v predchádzajúcej kapitole, term $\lambda x.x$ má nekonečné množstvo inštancií typu, pri ktorých je správne typovaný. Avšak v takomto prípade naším cieľom pri typovom odvodení nie je len nájsť "nejaký" typ, ale nájsť najvšeobecnejší typ.

Najvšeobecnejší typ (z ang. principal type) je taký typ, ktorý povoľuje vytvorenie najväčšieho množstva typových inštancií, ktoré vznikajú aplikáciou substitúcie.

Nájdenie najvšeobecnejšieho unifikátora prostredníctvom unifikačného algoritmu

Aby sme našli najvšeobecnejší typ potrebujeme nájsť najvšeobecnejšiu substitúciu (unifikátor) $\sigma$, ktorá bude spĺňať danú množinu obmedzení. Avšak nie vždy je množina obmedzení také prostá ako v predchádzajúcich príkladoch a nájdenie najvšeobecnejšieho unifikátora (ak vôbec existuje) sa stáva zložitým problémom.

Najvšeobecnejší unifikátor následne aplikujeme na odvodený typ a tým získame najvšeobecnejší typ.

Pre výpočet najvšeobecnejšieho unifikátora danej množiny obmedzení využijeme myšlienku Hindleyho a Milnera, ktorí na tento účel upravili Robinsonov unifikačný algoritmus.

Unifikačný algoritmus

Algoritmus: Unifikačný algoritmus

Vstup: Množina obmedzení $C$

Výstup: Najvšeobecnejší unifikátor $\sigma_{mgu}$ (ak existuje), zlyhanie inak

$$ \begin{array}{lll} unify(C) &=& if~C=\{\}, ~then~[~] \\ & & else \\ & & \quad \quad let~ \{S=T\} \cup C'=C~in \\ & & \quad if~ S=T \\ & & \quad \quad then ~ unify(C')\\ & & \quad else~if~ S=X ~a~ X\notin T \\ & & \quad \quad then ~ unify([X\mapsto T]C') \circ [X\mapsto T]\\ & & \quad else~if~ T=X ~a~ X\notin S \\ & & \quad \quad then ~ unify([X\mapsto S]C') \circ [X\mapsto S]\\ & & \quad else~if~ S=S_1 \rightarrow S_2 ~~and~~ T = T_1 \rightarrow T_2 \\ & & \quad \quad then ~ unify(C' \cup \{S_1=T_1, S_2 = T_2\}) \\ & & \quad else ~ fail \end{array} $$

Unifikačný algoritmus slovne

• Rekurzívne voláme funkciu $unify(C)$ pokiaľ množina obmedzení $C$ nie je prázdna $C=\{~\}$. Možnosti:
  • Priradenie novej substitúcie do $\sigma_{mgu}$.
  • Priradenie nového obmedzenia do $C$.
  • Fail, množina obmedzení $C$ je inkonzistentná.
• Vyberieme prvú rovnosť $S=T$ z množiny obmedzení $\{S=T\} \cup C'=C$ ($C'$ zvyšok množiny obmedzení).
  • Ak zvolená rovnosť je v tvare $T=T$, napr. $X=X, Nat=Nat, Nat\rightarrow Nat = Nat\rightarrow Nat...$.
    • Žiadne nové obmedzenie, ani substitúcia.
    • Voláme rekurzívne funkciu $unify(C')$ so zvyškom množiny obmedzení.
  • Ak vo zvolenej rovnosti $S=T$ je na pravej strane $X$ (*to znamená *$S=X$), a zároveň $X$ sa nenachádza v $T$, pričom $X$ je typová premenná:
    • Substitúcia $T$ za $X$ v množine obmedzení $C'$ - eliminácia typovej premennej $X$.
    • Rekurzívne volanie funkcie $unify([X\mapsto T]C') \circ [X\mapsto T]$ s aktualizovanou množinou obmedzení po substitúcii. Zároveň vzniká časť riešenia $unify(C) = \sigma_{mgu}= ... \circ [X\mapsto T]$.
  • Ak vo zvolenej rovnosti $S=T$ je na ľavej strane $X$ (*to znamená *$T=X$) a zároveň $X$ sa nenachádza v $S$, pričom $X$ je typová premenná:
    • Substitúcia $S$ za $X$ v množine obmedzení $C'$ - eliminácia typovej premennej $X$.
    • Rekurzívne volanie funkcie $unify([X\mapsto S]C') \circ [X\mapsto S]$ s aktualizovanou množinou obmedzení po substitúcii. Zároveň vzniká časť riešenia $unify(C) = \sigma_{mgu}= ... \circ [X\mapsto S]$.
  • Ak zvolená rovnosť je v tvare $T_1\rightarrow T_2 = S_1 \rightarrow S_2$
    • Pridáme nové obmedzenia do množiny obmedzení $C'$ v tvare: $T_1=S_1, T_2=S_2$.
    • Rekurzívne voláme $unify(C' \cup \{S_1=T_1, S_2 = T_2\})$.

GHCi, version 9.4.7: https://www.haskell.org/ghc/  :? for help
ghci> term = (\x -> x) (\y -> y)
ghci> :t term
term :: p -> p
ghci> term 2 
2
ghci> :t term 2
term 2 :: Num p => p
ghci> term "text"
"text"
ghci> :t term "text"
term "text" :: String

utop # let term = (fun x -> x) (fun y -> y);;
val term : '_weak1 -> '_weak1 = <fun>
utop # let id = fun x -> x;;
val id : 'a -> 'a = <fun>
utop # term 2;;
- : int = 2
utop # term ;;
- : int -> int = <fun>
utop # let term = (fun x -> x) (fun y -> y);;
val term : '_weak2 -> '_weak2 = <fun>
utop # term "text";;
- : string = "text"

Riešenie

1. Zostrojíme štruktúru typového stromu:

2. Podľa pravidiel doplníme typy a obmedzenia:

Z typového stromu sme získali nasledovné:

• Odvodený typ: $$S=A \rightarrow B \rightarrow F.$$
• Množina obmedzení: $$C=\{Nat \rightarrow Nat \rightarrow Nat = B \rightarrow D,~ D=Nat\rightarrow E,~ A=E \rightarrow F\}$$

Aplikujeme unifikačný algoritmus na množinu obmedzení $C$ a získame najvšeobecnejší unifikátor $\sigma_{mgu}$: $$unify(\{Nat \rightarrow Nat \rightarrow Nat = B \rightarrow D,~ D=Nat\rightarrow E,~ A=E \rightarrow F\})=\sigma_{mgu}$$

$Unify$ Iterácia	Množina obmedzení $C$
1.	$\{Nat \rightarrow Nat \rightarrow Nat = B \rightarrow D,~ D=Nat\rightarrow E,~ A=E \rightarrow F\}$
2.	$\{Nat = B,~ Nat \rightarrow Nat = D,~ D=Nat\rightarrow E,~ A=E \rightarrow F\}$
3.	$\{Nat \rightarrow Nat = D,~ D=Nat\rightarrow E,~ A=E \rightarrow F\}$
4.	$\{Nat \rightarrow Nat=Nat\rightarrow E,~ A=E \rightarrow F\}$
5.	$\{Nat=Nat,~ Nat = E,~ A=E \rightarrow F\}$
6.	$\{Nat = E,~ A=E \rightarrow F\}$
7.	$\{A=Nat \rightarrow F\}$
8.	$\{~\}$

Unifikáciou množiny obmedzení $C$ sme získali nasledujúci najvšeobecnejší unifikátor $\sigma_{mgu}$:

$$ \begin{array}{l} unify(\{Nat \rightarrow Nat \rightarrow Nat = B \rightarrow D,~ D=Nat\rightarrow E,~ A=E \rightarrow F\})= \\ [~]\circ [A \mapsto Nat \rightarrow F] \circ [E \mapsto Nat] \circ [D \mapsto Nat \rightarrow Nat] \circ [B \mapsto Nat]=\\ =\sigma_{mgu} \end{array} $$ Následne aplikujeme $\sigma_{mgu}$ na odvodený typ $S$ a získame najvšeobecnejší typ termu $t$ v typovom kontexte $\Gamma$:

$$\sigma_{mgu}(A \rightarrow B \rightarrow F)=(Nat \rightarrow F) \rightarrow Nat \rightarrow F.$$

Overíme naše riešenie prostredníctvom interpretéra jazyka OCaml:

utop # let add = fun x -> fun y -> x + y;;
val add : int -> int -> int = <fun>
utop # let t= fun f -> fun x -> f (add x 1);;
val t : (int -> 'a) -> int -> 'a = <fun>