Polymorfizmus
V predchádzajúcej prednáške sme zaviedli monomorfnú typovú rekonštrukciu pomocou typových premenných, generovania obmedzení a unifikácie. Každá viazaná termová premenná mala v celom svojom rozsahu jeden spoločný typ. Typová premenná v najvšeobecnejšom typovom výraze ešte sama nezavádzala polymorfizmus.
Ako môžeme jednu definíciu funkcie používať pri rôznych typoch? Identita napríklad vracia svoj argument bez ohľadu na to, či ide o prirodzené číslo alebo booleovskú hodnotu. Najprv predstavíme explicitný polymorfný λ-kalkul Systém F, potom let-polymorfizmus a jeho rozhodnuteľnú typovú rekonštrukciu.
Polymorfizmus umožňuje používať jednu programovú konštrukciu pri viacerých typoch. Jednotlivé druhy sa líšia tým, ako tieto typy vznikajú a či sa podľa typu mení aj implementácia.
Poznámka
Názov pochádza z gréckych slov poly (veľa) a morphé (tvar).
Druhy polymorfizmu
Existuje viacero druhov polymorfizmu, ktoré nie sú disjunktné, teda v jednom jazyku sa môže vyskytnúť viac druhov naraz.
Parametrický polymorfizmus
Jedna definícia pracuje jednotným spôsobom pre rôzne typy svojich parametrov. Typy sú parametrami, nie podnetom na výber odlišnej implementácie. V skúmanom čistom fragmente nemôže identita skúmať vnútornú štruktúru ľubovoľného argumentu.
Definícia: Monotyp a typová schéma
Monotyp $S$ je typový výraz bez univerzálnych kvantifikátorov. Môže obsahovať základné typy, typové konštanty, typové premenné a funkčné typy.
Typová schéma má tvar:
$$\forall\alpha_1.\cdots\forall\alpha_n.S.$$
Platí $n\in\mathbb N$ a kvantifikované premenné sú navzájom rôzne. Kvantifikátory sú iba na začiatku schémy a telo $S$ je monotyp. Pre $n=0$ je schémou samotný monotyp.
Napríklad $\alpha\to\alpha$ je monotyp, hoci obsahuje typovú premennú. Zápis $\forall\alpha.\alpha\to\alpha$ je polymorfná typová schéma.
Uvedený tvar typovej schémy využíva Hindleyho–Milnerov systém, ku ktorému sa dostaneme v druhej časti prednášky. V Systéme F, ktorý predstavíme najprv, môžu byť univerzálne kvantifikátory aj vnorené vo vnútri typových výrazov. Polymorfné typy Systému F teda nie sú obmedzené na prenexný tvar.
- Predikatívnosť obmedzuje, aké typy možno dosadzovať pri inštanciácii. V Hindleyho–Milnerovom systéme (HM) dosadzujeme iba monotypy bez univerzálnych kvantifikátorov.
- Prenexnosť obmedzuje polohu kvantifikátorov: nachádzajú sa iba vo vonkajšom prefixe typovej schémy. Od predikatívnosti sa líši tým, že určuje polohu kvantifikátorov, kým predikatívnosť obmedzuje typy prípustné pri inštanciácii. Systém HM spĺňa obe obmedzenia.
- Impredikatívnosť pripúšťa inštanciáciu aj samotným polymorfným typom. Systém F je polymorfný λ-kalkul druhého rádu a je impredikatívny.
Ad hoc polymorfizmus
Rovnaké meno môže označovať rôzne implementácie pre rôzne typy. Pri preťažení (overloading) sa vyberá vhodná implementácia podľa typov argumentov. Viacnásobný dynamický výber (multiple dispatch) môže vyberať implementáciu podľa skutočných typov viacerých argumentov počas vykonávania; nie je obmedzený iba na dynamicky typované jazyky.
Intenzionálny polymorfizmus
Dovoľuje obmedzene výpočty nad typmi v runtime. Používa sa pri implementačných technikách pre polymorfné jazyky (garbage collector, polymorfné usporiadanie).
Podtypový polymorfizmus
Poskytuje termu viac inštancií typov podľa pravidiel podtypovania. Používa sa v objektovo-orientovaných programovacích jazykoch.
Motivácia
Typová rekonštrukcia zo siedmej prednášky určuje pre typovateľný term najvšeobecnejší typový výraz. Prítomnosť typových premenných v tomto výraze však sama osebe nezavádza polymorfizmus: všetky výskyty jedného λ-viazaného parametra musia mať rovnaký typ. Táto požiadavka obmedzuje použitie funkcie odovzdanej ako argument, čo ilustruje nasledujúci príklad.
Príklad
Uvažujme term
$$ (\lambda f.\mathsf{if}\ f\ \mathsf{true}\ \mathsf{then}\ f\ 5\ \mathsf{else}\ f\ 8)\;(\lambda x.x). $$
1. Schéma typovacieho stromu. Označme $\Gamma_1=\{x:\beta\}$ a $\Gamma_2=\{f:\alpha\}$. Prvý strom zachytáva štruktúru pravidiel, nie hotové typovacie odvodenie:
2. Úplný typovací strom s obmedzeniami. Pri všetkých troch použitiach $f$ používame tú istú typovú premennú $\alpha$. Nové výsledkové premenné volíme navzájom rôzne:
Získame množinu obmedzení:
$$ C=\left\{\alpha=\mathsf{Bool}\to\gamma,\ \alpha=\mathsf{Nat}\to\delta,\ \alpha=\mathsf{Nat}\to\theta,\ \gamma=\mathsf{Bool},\ \delta=\theta,\ \alpha\to\delta=(\beta\to\beta)\to\zeta\right\}. $$
Poslednú rovnosť $\alpha\to\delta=(\beta\to\beta)\to\zeta$ rozložíme na $\alpha=\beta\to\beta$ a $\delta=\zeta$. Po dosadení do prvých dvoch rovností dostaneme:
$$\begin{aligned} \beta\to\beta&=\mathsf{Bool}\to\gamma,\\ \beta\to\beta&=\mathsf{Nat}\to\delta. \end{aligned}$$
Premenná $\beta$ by musela byť zároveň $\mathsf{Bool}$ aj $\mathsf{Nat}$. Unifikácia preto zlyhá. Už samotné dva nároky na vstupný typ monomorfného $f$ sú nezlučiteľné.
OCaml tento problém potvrdzuje:
utop # (fun f -> if f true then f 5 else f 8) (fun x -> x);;
Error: This expression has type int
but an expression was expected of type bool
Bez typovej kontroly sa tento term vyhodnotí na $5$: identita v podmienke vráti $\mathsf{true}$, preto sa vyberie vetva $f\ 5$. Výpočet teda dá výsledok, hoci monomorfný typový systém term odmietne.
Na vyjadrenie funkcie použiteľnej pri rôznych typoch potrebujeme pravidlá polymorfizmu. V Systéme F ich vyjadríme univerzálne kvantifikovaným typom a explicitnými typovými operáciami.
Systém F
Systém F nezávisle zaviedli Jean-Yves Girard (1972) a John C. Reynolds (1974). Nazýva sa aj polymorfný λ-kalkul alebo λ-kalkul druhého rádu. Podľa Curryho–Howardovej korešpondencie možno typy chápať ako logické tvrdenia a termy ako ich dôkazy. Univerzálne kvantifikovaný typ potom zodpovedá tvrdeniu, ktoré platí pre každý dosadený typ.
Oproti STLC pridávame typovú abstrakciu $\Lambda\alpha.t$, typovú aplikáciu $t[T]$ a typový konštruktor $\forall\alpha.T$. Rozlišujeme termový parameter v $\lambda x:T.t$ a typový parameter v $\Lambda\alpha.t$.
Definícia: Polymorfný typ v Systéme F
Typ $\forall\alpha.T$ viaže typovú premennú $\alpha$ v type $T$. Term tohto typu možno inštanciovať ľubovoľným platným typom $U$; výsledný typ je $[\alpha\mapsto U]T$. Kvantifikácia môže byť vnorená aj v ďalších typových konštruktoroch.
Napríklad $(\forall\alpha.\alpha\to\alpha)\to(\forall\alpha.\alpha\to\alpha)$ je funkčný typ, ktorého vstupom aj výstupom je polymorfná funkcia.
Poznámka
Každý z oboch kvantifikátorov viaže typovú premennú iba vo svojom rozsahu. Rovnaké meno $\alpha$ preto neznamená, že ide o tú istú viazanú premennú. Viazané premenné môžeme nezávisle premenovať, napríklad na $\alpha$ v prvom type a $\beta$ v druhom:
$$(\forall\alpha.\alpha\to\alpha)\to(\forall\beta.\beta\to\beta).$$
Tento zápis je s pôvodným typom $\alpha$-ekvivalentný.
Syntax Systému F
Výsledná syntax Systému F je definovaná nasledovne:
$$ \begin{array}{lcl} t & ::= & x ~|~ \lambda x:T.t ~|~ t~t ~|~ \Lambda\alpha.t ~|~ t[T] \\ v & ::= & \lambda x:T.t ~|~ \Lambda\alpha.t \\ T & ::= & \alpha ~|~ T\rightarrow T ~|~ \forall\alpha.T \\ \Gamma & ::= & \epsilon ~|~ \Gamma,\alpha ~|~ \Gamma,x:T \end{array} $$
- Typové premenné: $\alpha,\beta,\gamma,\ldots\in\chi$. Typové výrazy označujeme $S,T,U$.
- Kontext: $\Gamma$ je usporiadaný zoznam deklarácií typových premenných a termových predpokladov $x:T$. Prázdny kontext označujeme $\epsilon$.
- Platnosť kontextu: kontext je platný, ak sa v ňom žiadne meno neopakuje a všetky voľné typové premenné typu v každej deklarácii $x:T$ sú deklarované už v predchádzajúcej časti kontextu. Prázdny kontext $\epsilon$ je platný. Napríklad $\alpha,x:\alpha$ je platný kontext, ale $x:\alpha,\alpha$ platný nie je: pri deklarácii $x:\alpha$ ešte typová premenná $\alpha$ nebola deklarovaná. Konflikt mien riešime premenovaním viazanej premennej.
- Platnosť typu: všetky jeho voľné typové premenné musia byť deklarované v $\Gamma$. Pri type $\forall\alpha.T$ overujeme telo $T$ v kontexte $\Gamma,\alpha$, kde je $\alpha$ čerstvá.
- Rozsah a asociativita: funkčné typy sú pravoasociatívne; rozsah kvantifikátora aj abstrakcie siaha čo najviac doprava. Typy porovnávame až na premenovanie viazaných typových premenných.
- Čistý Systém F: jazyk neobsahuje základné typy ani číselné a booleovské konštanty. V príkladoch ich najprv predpokladáme a potom ich definujeme Churchovým kódovaním, pričom názvy kódovaní sú metajazykové skratky.
Statická sémantika – typovacie pravidlá
Typová abstrakcia. Pri zavedení $\forall\alpha$ musí byť $\alpha$ nezávislá od typov termových predpokladov. V zmiešanom kontexte to zabezpečuje čerstvá deklarácia $\alpha$: staršie termové predpoklady na nej nemôžu závisieť.
$\alpha\notin\Gamma$; kontexty sú platné.
Kontext $\Gamma$ musí byť platný a typová premenná $\alpha$ v ňom ešte nesmie byť deklarovaná. Typy premenných deklarovaných v $\Gamma$ preto nemôžu závisieť od novej premennej $\alpha$.
Typová aplikácia. Term $t$ typu $\forall\alpha.T$ môžeme použiť pre zvolený typ $U$ zápisom $t[U]$. Jeho výsledný typ získame dosadením $U$ za voľné výskyty $\alpha$ v $T$. Za $U$ môžeme zvoliť aj polymorfný typ, napríklad $\forall\beta.\beta\to\beta$; typový argument teda môže sám obsahovať univerzálny kvantifikátor.
$U$ je platný typ v $\Gamma$; dosadenie nezachytáva premenné.
Pravidlá T-Var, T-Abs a T-App zostávajú rovnaké ako v STLC, pričom všetky kontexty a typy musia byť platné.
Príklad
Predpokladajme, že $\mathsf{Nat}$ označuje nejaký uzavretý typ Systému F.
Nech $id=\Lambda\alpha.\lambda x:\alpha.x$ označuje polymorfnú identitu typu $\forall\alpha.\alpha\to\alpha$. Pre každý zvolený typ argumentu vracia výsledok rovnakého typu.
Typovou aplikáciou $id[T]$ vytvoríme inštanciu identity pre typ $T$. Typ $T$ uvedený v hranatých zátvorkách dosadíme za viazanú premennú $\alpha$ v type identity. Takto získanej funkcii môžeme následne odovzdať termový argument typu $T$. Napríklad:
$$id[\mathsf{Nat}]:\mathsf{Nat}\to\mathsf{Nat}.$$
V Systéme F môžeme za $\alpha$ zvoliť aj typ $\forall\alpha.\alpha\to\alpha$, teda typ polymorfnej identity. Nahradíme ním oba výskyty $\alpha$ vo funkčnom type $\alpha\to\alpha$:
$$[\alpha\mapsto(\forall\alpha.\alpha\to\alpha)](\alpha\to\alpha)=(\forall\alpha.\alpha\to\alpha)\to(\forall\alpha.\alpha\to\alpha).$$
Preto platí:
$$id[\forall\alpha.\alpha\to\alpha]:(\forall\alpha.\alpha\to\alpha)\to(\forall\alpha.\alpha\to\alpha).$$
Takto inštanciovaná identita prijíma polymorfnú funkciu a vracia tú istú funkciu. Výraz $id[\forall\alpha.\alpha\to\alpha]$ ju zatiaľ iba pripravuje na tento typ argumentu; ešte jej neodovzdáva žiadnu funkciu. Impredikatívnosť spočíva v tom, že za typovú premennú smieme dosadiť aj typ obsahujúci univerzálny kvantifikátor.
Dynamická sémantika – vyhodnocovacie pravidlá
Aj pre Systém F zvolíme volanie hodnotou, čím nadviažeme na vyhodnotenie v predchádzajúcich jazykoch. Typovú abstrakciu $\Lambda\alpha.t$ považujeme za hodnotu a v jej tele nevykonávame žiadne kroky. Pri vyhodnotení typovej aplikácie $t[T]$ najprv vyhodnotíme term $t$; keď získame typovú abstrakciu, dosadíme do jej tela typ $T$ za viazanú typovú premennú. Samotný typový argument $T$ sa nevyhodnocuje.
Substitúcia $[\alpha\mapsto T]t$ nahrádza typom $T$ voľné výskyty typovej premennej $\alpha$ v typových anotáciách a typových argumentoch termu $t$. Termové premenné nemení. V rozsahu typovej abstrakcie $\Lambda\alpha$ alebo univerzálneho kvantifikátora $\forall\alpha$ za $\alpha$ nedosádzame, pretože tam už ide o viazanú premennú. Ak by sa voľná typová premenná z $T$ po dosadení stala viazanou, najprv príslušnú viazanú typovú premennú premenujeme na čerstvú.
Napríklad $[\alpha\mapsto\beta](\forall\beta.\alpha\to\beta)=\forall\gamma.\beta\to\gamma$ pre čerstvé $\gamma$. Podobné premenovanie je potrebné aj pri dosadení do termu $\Lambda\beta.\lambda x:\alpha.x$.
Poznámka
Pravidlá vyhodnotenia termovej aplikácie preberáme z jednoducho typovaného λ-kalkulu s volaním hodnotou.
Príklad
Nech je $id$ metajazyková skratka polymorfnej identity:
$$id=\Lambda\alpha.\lambda x:\alpha.x,\qquad\vdash id:\forall\alpha.\alpha\to\alpha.$$
Predpokladajme, že máme uzavretý typ $\mathsf{Nat}$ a uzavretú hodnotu $\mathbf{3}:\mathsf{Nat}$.
Typovou aplikáciou získame term typu $\mathsf{Nat}\to\mathsf{Nat}$:
$$id[\mathsf{Nat}]\to\lambda x:\mathsf{Nat}.x.$$
Po dodaní termového argumentu vyhodnotíme aplikáciu:
$$id[\mathsf{Nat}]\ \mathbf{3}\to(\lambda x:\mathsf{Nat}.x)\ \mathbf{3}\to\mathbf{3}.$$
Príklady typovania v Systéme F
Príklad
Odvoďte typ termu $\Lambda\alpha.\lambda x:\alpha.x$. V tomto príklade $\Gamma_1=(\alpha,x:\alpha)$.
1. Schéma typovacieho stromu. Podmienka T-TAbs platí, pretože vonkajší kontext je prázdny:
2. Úplný typovací strom. V T-Abs odstránime termový predpoklad $x:\alpha$, potom v T-TAbs typovú deklaráciu $\alpha$:
Príklad
Predpokladajme, že máme uzavretý typ $\mathsf{Bool}$ a uzavretú hodnotu $\mathsf{true}:\mathsf{Bool}$.
Odvoďte typ termu
$$ (\Lambda\alpha.\lambda x:\alpha.x)[\mathsf{Bool}]\ \mathsf{true}. $$
1. Schéma typovacieho stromu. Označme $\Gamma_1=(\alpha,x:\alpha)$. Ľavá vetva obsahuje celú typovú abstrakciu identity:
2. Typová inštanciácia. Pravidlo T-TApp dosadí typový argument za viazanú premennú:
$$[\alpha\mapsto\mathsf{Bool}](\alpha\to\alpha)=\mathsf{Bool}\to\mathsf{Bool}.$$
3. Úplný typovací strom. Po dosadení typu $\mathsf{Bool}$ za typovú premennú $\alpha$ uzavrieme typovací strom pravidlom T-App:
Výsledný typ je $\mathsf{Bool}$. Typová aplikácia a následná termová aplikácia sú dva odlišné kroky.
Churchove booleovské hodnoty a čísla v Systéme F
Doteraz sme existenciu typov $\mathsf{Bool}$ a $\mathsf{Nat}$ a ich hodnôt iba predpokladali. Teraz ich definujeme pomocou typovej kvantifikácie a funkcií Systému F. Zavedené názvy budú skratkami týchto definícií.
Churchove booleovské hodnoty
Booleovská hodnota vyberá jeden z dvoch argumentov rovnakého typu. Typ aj obe hodnoty definujeme:
$$\mathsf{Bool}=\forall\alpha.\alpha\to\alpha\to\alpha.$$
$$\begin{aligned} \mathsf{true}&=\bigl(\Lambda\alpha.\lambda x:\alpha.\lambda y:\alpha.x\bigr):\mathsf{Bool},\\ \mathsf{false}&=\bigl(\Lambda\alpha.\lambda x:\alpha.\lambda y:\alpha.y\bigr):\mathsf{Bool}. \end{aligned}$$
Negácia vymení poradie argumentov:
$$\mathsf{not}=\bigl(\lambda b:\mathsf{Bool}.\Lambda\alpha.\lambda x:\alpha.\lambda y:\alpha.b[\alpha]\ y\ x\bigr):\mathsf{Bool}\to\mathsf{Bool}.$$
Zápis $\mathsf{Bool}\to\mathsf{Bool}$ rozvíjame na $(\forall\alpha.\alpha\to\alpha\to\alpha)\to(\forall\alpha.\alpha\to\alpha\to\alpha)$. Pre term $b:\mathsf{Bool}$, platný typ $T$ a termy $u:T$, $v:T$ má $b[T]\ u\ v$ typ $T$; takto sa v kódovaní vyjadruje výber vetvy bez pridania konštrukcie $\mathsf{if}$ do syntaxe.
Churchove prirodzené čísla
Churchove numerály. Prirodzené číslo predstavuje počet opakovaní funkcie nad počiatočnou hodnotou. Definujeme:
$$\mathsf{Nat}=\forall\alpha.(\alpha\to\alpha)\to\alpha\to\alpha.$$
$$\begin{aligned} \mathbf{0}&=\bigl(\Lambda\alpha.\lambda f:\alpha\to\alpha.\lambda x:\alpha.x\bigr):\mathsf{Nat},\\ \mathbf{1}&=\bigl(\Lambda\alpha.\lambda f:\alpha\to\alpha.\lambda x:\alpha.f\ x\bigr):\mathsf{Nat},\\ \mathbf{3}&=\bigl(\Lambda\alpha.\lambda f:\alpha\to\alpha.\lambda x:\alpha.f\ (f\ (f\ x))\bigr):\mathsf{Nat},\\ &\vdots\\ \mathbf{n}&=\bigl(\Lambda\alpha.\lambda f:\alpha\to\alpha.\lambda x:\alpha.f^n x\bigr):\mathsf{Nat}. \end{aligned}$$
Pre ľubovoľné $n\in\mathbb{N}$ zápis $f^n x$ označuje $n$ opakovaných aplikácií funkcie $f$ na počiatočnú hodnotu $x$: $f^0x=x$ a $f^{n+1}x=f\,(f^n x)$. Pre $n=0$ je teda telom iba $x$.
Nasledovník vykoná o jednu aplikáciu $f$ viac:
$$\mathsf{succ}=\bigl(\lambda n:\mathsf{Nat}.\Lambda\alpha.\lambda f:\alpha\to\alpha.\lambda x:\alpha.f\ (n[\alpha]\ f\ x)\bigr):\mathsf{Nat}\to\mathsf{Nat}.$$
Sčítanie možno definovať pomocou iterácie nasledovníka:
$$\mathsf{plus}_{iter}=\bigl(\lambda m:\mathsf{Nat}.\lambda n:\mathsf{Nat}.m[\mathsf{Nat}]\ \mathsf{succ}\ n\bigr):\mathsf{Nat}\to\mathsf{Nat}\to\mathsf{Nat}.$$
Typovou aplikáciou $m[\mathsf{Nat}]$ volíme ako stav iterácie celý polymorfný typ $\mathsf{Nat}$. Ide o impredikatívnu inštanciáciu. Funkciu $\mathsf{succ}$ aplikujeme $m$-krát, pričom začíname numerálom $n$.
Rovnaké sčítanie možno vyjadriť priamo skladaním iterácií:
$$\mathsf{plus}_{direct}=\bigl(\lambda m:\mathsf{Nat}.\lambda n:\mathsf{Nat}.\Lambda\alpha.\lambda f:\alpha\to\alpha.\lambda x:\alpha.m[\alpha]\ f\ (n[\alpha]\ f\ x)\bigr):\mathsf{Nat}\to\mathsf{Nat}\to\mathsf{Nat}.$$
Najprv sa na $x$ aplikuje $f$ celkovo $n$-krát a potom ešte $m$-krát. Termy $\mathsf{plus}_{iter}$ a $\mathsf{plus}_{direct}$ majú ten istý uvedený typ a na Churchových numeráloch realizujú rovnakú operáciu sčítania, hoci sú syntakticky rôzne. Čísla $m,n$ v tomto vysvetlení označujú počty opakovaní; termové parametre $m,n$ v definíciách sú Churchove numerály.
Poznámka
Podľa princípov z prednášky 2 možno obdobne definovať ďalšie Churchove kombinátory, napríklad booleovské operácie, násobenie, predchodcu či test na nulu. V Systéme F pritom doplníme príslušné typové anotácie, typové abstrakcie a typové aplikácie a overíme typovanie výsledných termov.
Sebaaplikácia a Systém F
V monomorfnom STLC má pri rekonštrukcii term $\lambda x.x\ x$ dva výskyty parametra s rovnakým typom $\alpha$. Aplikácia vynúti rovnosť $\alpha=\alpha\to\beta$, ktorú kontrola výskytu odmietne.
Príklad
Pre $\Gamma=\{x:\alpha\}$ dostaneme úplný strom s obmedzeniami:
Obe vetvy CT-Var sú platné, ale výsledná množina obmedzení nemá riešenie medzi konečnými jednoduchými typmi. Neúspech nespočíva v názve premennej ani v chýbajúcej deklarácii.
Zápis $\lambda x.x\ x$ nezodpovedá syntaxi explicitného Systému F, pretože pri parametri $x$ chýba typová anotácia. Sebaaplikáciu môžeme vyjadriť pomocou polymorfného typu parametra a explicitnej typovej aplikácie:
$$\lambda x:(\forall\alpha.\alpha\to\alpha).\,x[\forall\alpha.\alpha\to\alpha]\ x.$$
Parameter $x$ má pri oboch výskytoch ten istý polymorfný typ. Ľavý výskyt inštanciujeme celým typom $\forall\alpha.\alpha\to\alpha$, takže vznikne funkcia prijímajúca práve pravý výskyt $x$. Toto je impredikatívna inštanciácia.
Príklad
Označme $\Gamma=\{x:\forall\alpha.\alpha\to\alpha\}$.
1. Schéma typovacieho stromu. Typový argument aj anotácia parametra sú súčasťou termu:
2. Úplný typovací strom. Typ parametra aj typ dosadený v typovej aplikácii sú $\forall\alpha.\alpha\to\alpha$:
V ľavej vetve T-TApp vypočíta:
$$[\alpha\mapsto(\forall\alpha.\alpha\to\alpha)](\alpha\to\alpha)=(\forall\alpha.\alpha\to\alpha)\to(\forall\alpha.\alpha\to\alpha).$$
Pravidlo T-App dá telu typ $\forall\alpha.\alpha\to\alpha$ a T-Abs pridá vstupný typ parametra. Po vymazaní anotácie a typovej aplikácie získame pôvodnú sebaaplikáciu.
Fragmenty Systému F a rozhodnuteľnosť typových problémov
Typová kontrola dostáva term a očakávaný typ. Pre plne anotovaný Churchovský Systém F je rozhodnuteľná: pravidlá nasledujú štruktúru termu a typové argumenty sú explicitné. Rovnako možno vypočítať typ takéhoto úplného termu.
Typová rekonštrukcia hľadá chýbajúce typové informácie. V Curryho štýle Systému F pracujeme s termami bez explicitných typových operácií a anotácií. Otázka, či taký term má vôbec nejaký typ, je nerozhodnuteľná. V tomto štýle je nerozhodnuteľná aj otázka, či neanotovaný term má konkrétne zadaný typ. Neexistuje všeobecný algoritmus, ktorý pre každý vstup skončí a správne odpovie; nejde iba o potrebu doplniť niekoľko anotácií. Tento výsledok preukázal J. B. Wells.
Pri kontrole dostávame term aj typ a rozhodujeme, či k sebe patria. Pri rekonštrukcii dostávame term s chýbajúcimi typovými údajmi a hľadáme jeho typ. Rozhodnuteľnosť znamená, že existuje algoritmus, ktorý skončí na každom vstupe so správnou odpoveďou. Výsledky závisia od toho, aké informácie vstup obsahuje:
| Systém a zadaný term | Kontrola zadaného typu | Zistenie typu termu |
|---|---|---|
| Monomorfný STLC; anotácie parametrov môžu chýbať | Rozhodnuteľná: zadaný typ možno overiť spolu s obmedzeniami. | Rozhodnuteľná: generovanie rovností a unifikácia nájdu najvšeobecnejší typový výraz, alebo term odmietnu. |
| Churchovský Systém F; všetky anotácie, typové abstrakcie a typové aplikácie sú explicitné | Rozhodnuteľná: pravidlá určia typ termu a porovnajú ho so zadaným typom. | Typ úplného termu možno vypočítať. Tento vstup už obsahuje všetky typové argumenty; nejde o rekonštrukciu z neanotovaného termu. |
| Curryho Systém F; λ-term bez explicitných typových údajov | Nerozhodnuteľná: ani pri zadanom type neexistuje všeobecný rozhodovací algoritmus. | Nerozhodnuteľná: všeobecne nemožno algoritmicky rozhodnúť ani to, či term má nejaký typ Systému F. |
| Hindleyho–Milnerov systém; term s let-definíciami a implicitnými schémami | Rozhodnuteľná: zadaný monotyp možno overiť pomocou rekonštrukcie. | Rozhodnuteľná: algoritmus nájde najvšeobecnejšiu schému alebo term odmietne. Umožňujú to obmedzenia generalizácie a inštanciácie. |
Poznámka
Churchov a Curryho štýl Systému F sa líšia tým, ktoré typové údaje sú súčasťou termu:
- V Churchovom štýle píšeme anotácie parametrov aj typové operácie explicitne: $\Lambda\alpha.\lambda x:\alpha.x$. Z termu vieme určiť, kde sa zavádza typový parameter a akým typom sa inštanciuje.
- V Curryho štýle má tá istá identita zápis $\lambda x.x$. Typ $\forall\alpha.\alpha\to\alpha$ jej priraďujeme typovacími pravidlami; chýbajúce typové abstrakcie a aplikácie nie sú zapísané v terme.
Preto rozhodnuteľná kontrola úplného Churchovského termu nerieši problém hľadania typových údajov pre Curryho term. V druhom prípade ich musí systém ešte nájsť a tento všeobecný problém je nerozhodnuteľný.
Systém HM zachováva rozhodnuteľnú typovú rekonštrukciu vďaka obmedzeniam polymorfizmu: kvantifikátory sa nachádzajú iba vo vonkajšom prefixe typových schém, generalizácia sa vykonáva pri väzbách let a pri inštanciácii sa dosadzujú iba monotypy. Termy jazyka HM možno preložiť do explicitného Systému F doplnením typových abstrakcií a typových aplikácií. Väzba let pritom nie je súčasťou syntaxe explicitného Systému F, ale pri preklade sa vyjadrí jeho konštrukciami. V nasledujúcej sekcii zavedieme let-polymorfizmus a vysvetlíme pravidlá generalizácie a inštanciácie, na ktorých je systém HM založený.
Vlastnosti Systému F
Pre čistý Systém F platia nasledujúce dôležité metateoretické vlastnosti. Ich úplné dôkazy presahujú rozsah tejto prednášky, preto uvedieme iba ich formulácie a význam.
- Zachovanie typu (preservation): ak $\Gamma\vdash t:T$ a $t\to t'$, potom $\Gamma\vdash t':T$. Jeden krok vyhodnotenia nemení typ termu.
- Progres (progress): ak $\epsilon\vdash t:T$, potom je $t$ hodnotou alebo existuje term $t'$, pre ktorý $t\to t'$. Uzavretý správne typovaný term sa pri vyhodnocovaní nezasekne.
- Silná normalizácia (strong normalization): každý správne typovaný term má iba konečné redukčné postupnosti. Vyhodnocovanie uzavretého správne typovaného termu preto skončí hodnotou.
Zachovanie typu a progres spolu zabezpečujú typovú bezpečnosť. Silná normalizácia je samostatná, silnejšia vlastnosť týkajúca sa ukončenia redukčných postupností; zo samotného zachovania typu a progresu nevyplýva. Vylučuje nekonečné výpočty, preto kombinátor všeobecnej rekurzie, akým je $Y$, v čistom Systéme F nemožno typovať. Typovateľnosť anotovanej sebaaplikácie z predchádzajúceho príkladu s tým nie je v rozpore: tento term neslúži na všeobecnú rekurziu. Prehľad týchto vlastností uvádza aj výklad Systému F.
Poznámka
V nasledujúcej kapitole rozšírime typovú rekonštrukciu zo siedmej prednášky o let-polymorfizmus. Zachováme generovanie rovností a unifikačný algoritmus. Pri väzbe let umožníme vhodné typové premenné odvodeného typu generalizovať na polymorfnú schému. Pri každom výskyte takto zavedenej premennej potom kvantifikované typové premenné schémy nahradíme novými typovými premennými. Jednotlivé použitia tej istej definície tak môžu mať odlišné typy.
Let-polymorfizmus a Hindleyho–Milnerov systém
Vraciame sa k jazyku zo siedmej prednášky a rozšírime ho o nerekurzívny výraz $\mathsf{let}\ x=t_1\ \mathsf{in}\ t_2$. Výsledný typový systém nazývame Hindleyho–Milnerov systém (HM). Umožňuje používať jednu let-definíciu pri rôznych typoch a zachováva rozhodnuteľnú typovú rekonštrukciu.
Poznámka
Nerekurzívna väzba znamená, že nové meno $x$ je viazané iba v tele $t_2$, nie v definovanom terme $t_1$. Term $t_1$ sa teda nemôže odvolávať na práve zavádzanú definíciu $x$.
Vnorené väzby let sú prípustné. Napríklad v terme
$$\mathsf{let}\ x=0\ \mathsf{in}\ \mathsf{let}\ y=\mathsf{succ}\ x\ \mathsf{in}\ y$$
definícia $y$ používa už zavedené $x$; nejde o rekurziu. Rekurzívna väzba by umožnila odvolávať sa na definované meno aj v jeho vlastnej definícii, napríklad funkcii volať samu seba. Takúto väzbu tu nezavádzame.
Parameter funkcie má v HM jeden monotyp. Pri let-definícii môžeme vhodné typové premenné generalizovať na schému; pri každom použití definície potom vytvoríme jej čerstvú monotypovú inštanciu. Klasický algoritmus rekonštrukcie HM sa nazýva algoritmus W. Tu zachováme postup pomocou obmedzení a unifikácie zo siedmej prednášky.
Typy $\mathsf{Nat}$ a $\mathsf{Bool}$ v tejto časti opäť označujú základné typy STLC. Monotypy označujeme $S$ a typy vrátane typových schém označujeme $T$. Úplná syntax jazyka je:
$$ \begin{aligned} t&::=x\mid\lambda x:S.t\mid\lambda x.t\mid t\ t\mid0\mid\mathsf{true}\mid\mathsf{false}\mid\mathsf{succ}\ t\mid\mathsf{pred}\ t\\ &\phantom{{}::={}}\mid\mathsf{iszero}\ t\mid\mathsf{if}\ t\ \mathsf{then}\ t\ \mathsf{else}\ t\mid\mathsf{let}\ x=t\ \mathsf{in}\ t,\\ v&::=\lambda x:S.t\mid\lambda x.t\mid\mathsf{true}\mid\mathsf{false}\mid nv,\\ nv&::=0\mid\mathsf{succ}\ nv,\\ S&::=a\mid b\mid\alpha\mid S\to S,\qquad a\in\mathcal A,\\ T&::=S\mid\forall\alpha.T,\\ b&::=\mathsf{Nat}\mid\mathsf{Bool},\\ \Gamma&::=\epsilon\mid\Gamma,x:T. \end{aligned} $$
- Konštanty $a\in\mathcal A=\{A,B,C,\ldots\}$ sa pri unifikácii nemenia.
- Kontext priraďuje termovým premenným typy $T$. Polymorfizmus zavádzame iba generalizáciou pri väzbe
let. Parameter λ-abstrakcie dostáva monotyp $S$, ktorý sa negeneralizuje; všetky výskyty tohto parametra preto používajú rovnaký typ. Každé nové meno musí byť odlišné od mien už deklarovaných v kontexte.
Gramatika HM povoľuje univerzálne kvantifikátory iba na začiatku celého typu. Každý typ $T$ má preto tvar
$$T=\forall\alpha_1.\cdots\forall\alpha_n.S,\qquad n\in\mathbb N,$$
kde $S$ je monotyp, ktorý neobsahuje žiadny univerzálny kvantifikátor. Kvantifikátory tvoria prefix pred celým monotypom; nemôžu sa nachádzať v argumente ani vo výsledku funkčného typu. Takto obmedzený polymorfizmus nazývame prenexný polymorfizmus. Pre $n=0$ ide o samotný monotyp $S$.
Na rozdiel od Systému F preto $(\forall\alpha.\alpha\to\alpha)\to\mathsf{Nat}$ nie je prípustným typom HM: kvantifikátor sa v ňom nachádza v argumente funkčného typu. Explicitné anotácie parametrov, ak sú uvedené, sú monotypy; termy $\Lambda\alpha.t$ a $t[U]$ do tohto povrchového jazyka nepatria.
Pravidlo pre let-väzbu
Pravidlá pre abstrakciu, aplikáciu, booleovské výrazy a prirodzené čísla zostávajú rovnaké ako v siedmej prednáške. Pridávame pravidlo CT-Let; pravidlo pre použitie premennej nižšie rozšírime o inštanciáciu schémy. Pre monotypovú deklaráciu sa zhoduje s pôvodným CT-Var.
Najprv odvodíme $\Gamma\vdash t_1:S_1\mid C_1$. Funkcia $generalize$ vyrieši $C_1$, aktualizuje kontext a pridá deklaráciu $x$. Až potom spracujeme $t_2$ v takto získanom kontexte:
$\sigma_1=unify(C_1)$; unifikácia musí uspieť a $x$ je čerstvé v kontexte.
Zápis $\sigma_1 t_2$ upravuje prípadné existujúce typové anotácie v druhej vetve; neanotované termy nemení. Generalizácia prebieha po vyriešení $C_1$ a pred rekonštrukciou $t_2$.
Množina $\{\alpha=\sigma_1(\alpha)\mid\alpha\in\operatorname{dom}(\sigma_1)\}$ v závere explicitne zaznamenáva už vypočítanú substitúciu prvej vetvy v podobe rovností. Nahrádza pôvodné $C_1$ jeho vyriešeným tvarom. Záver teda obsahuje uložené riešenie prvej vetvy a zostávajúce obmedzenia $C_2$, nie dve nezávisle vygenerované nevyriešené množiny.
Pri sekvenčnom riešení uchováme $\sigma_1$ a vypočítame:
$$\sigma_2=unify(C_2),\qquad\sigma=\sigma_2\circ\sigma_1.$$
Obmedzenia $C_2$ už vznikli v aktualizovanom kontexte a z termu $\sigma_1t_2$, preto na ne $\sigma_1$ znova neaplikujeme. Kompozícia zachováva riešenie $C_1$ a súčasne spĺňa $C_2$; ak niektorá unifikácia zlyhá, rekonštrukcia zlyhá. Výsledný typ celého let-termu je $T=\sigma_2(S_2)$ a výsledný vonkajší kontext je $\sigma_2(\Gamma_1)=\sigma(\Gamma)$, kde $\Gamma_1=\sigma_1(\Gamma)$. Typ $S_2$ už pochádza z aktualizovanej druhej vetvy.
Generalizácia
Definícia: Voľné typové premenné schémy a kontextu
Funkcia $FTV$ vracia množinu voľných typových premenných. Definujeme ju pre všetky tvary monotypov, schém aj kontextov:
$$\begin{aligned} FTV(\alpha)&=\{\alpha\},\\ FTV(a)&=\emptyset,\qquad a\in\mathcal A,\\ FTV(b)&=\emptyset,\qquad b\in\{\mathsf{Nat},\mathsf{Bool}\},\\ FTV(S_1\to S_2)&=FTV(S_1)\cup FTV(S_2),\\ FTV(\forall\alpha.T)&=FTV(T)\setminus\{\alpha\},\\ FTV(\epsilon)&=\emptyset,\\ FTV(\Gamma,x:T)&=FTV(\Gamma)\cup FTV(T). \end{aligned}$$
Posledné pravidlo čítame takto: pri pridaní deklarácie $x:T$ vezmeme voľné typové premenné pôvodného kontextu a pridáme voľné typové premenné novej schémy. Samotné meno termovej premennej $x$ do tejto množiny nepatrí. Premenné viazané kvantifikátorom v schéme sa nepridávajú.
Napríklad pre $\Gamma=\{y:\alpha,\ f:\forall\beta.\beta\to\gamma\}$ platí $FTV(\Gamma)=\{\alpha,\gamma\}$. Premenná $\beta$ je v schéme funkcie $f$ viazaná.
Typová substitúcia mení iba voľné typové premenné schémy; v prípade potreby najprv premenuje viazané premenné proti zachyteniu. Na kontext ju aplikujeme v každej deklarácii.
Definícia: Zovšeobecnenie kontextu
Funkcia $generalize(C_1,\Gamma,x:S_1)$ spracuje obmedzenia definície a vráti aktualizovaný kontext rozšírený o deklaráciu $x$. Najprv vypočítame:
$$\sigma_1=unify(C_1),\qquad U_1=\sigma_1(S_1),\qquad\Gamma_1=\sigma_1(\Gamma).$$
Ak unifikácia zlyhá, funkcia nemá výsledok. Inak definujeme:
$$generalize(C_1,\Gamma,x:S_1)=\begin{cases} \begin{array}{l}\Gamma_1,x:\forall\alpha_1.\cdots\forall\alpha_n.U_1,\\\quad\text{ak }FTV(U_1)\setminus FTV(\Gamma_1)=\{\alpha_1,\ldots,\alpha_n\},\ n>0,\end{array}\\[0.8em] \begin{array}{l}\Gamma_1,x:U_1,\\\quad\text{ak }FTV(U_1)\setminus FTV(\Gamma_1)=\emptyset.\end{array} \end{cases}$$
Mená $\alpha_1,\ldots,\alpha_n$ sú navzájom rôzne a $x$ je čerstvé v kontexte. Poradie kvantifikovaných premenných zvolíme pevne.
Výpočet má tri nadväzujúce kroky:
- Vyriešenie obmedzení. Najvšeobecnejší unifikátor $\sigma_1$ musí spĺňať všetky rovnosti z $C_1$. Jeho aplikáciou na predbežný typ $S_1$ získame $U_1=\sigma_1(S_1)$.
- Aktualizácia kontextu. Tú istú substitúciu aplikujeme aj na všetky voľné typové premenné schém v pôvodnom kontexte: $\Gamma_1=\sigma_1(\Gamma)$. Vynechanie tohto kroku by mohlo viesť k nesprávnej generalizácii.
- Generalizácia a rozšírenie. Kvantifikujeme práve premenné z $FTV(U_1)\setminus FTV(\Gamma_1)$. Premenné voľné v aktualizovanom kontexte zostávajú spoločné s jeho predpokladmi, preto ich nemožno nezávisle inštanciovať. Ak je rozdiel prázdny, pridáme iba monotyp $x:U_1$.
Vzniknutú schému označme $\Sigma=\forall\alpha_1.\cdots\forall\alpha_n.U_1$, kde $\{\alpha_1,\ldots,\alpha_n\}=FTV(U_1)\setminus FTV(\Gamma_1)$; pre $n=0$ je $\Sigma=U_1$. Druhú vetvu pravidla CT-Let teda spracujeme v kontexte $generalize(C_1,\Gamma,x:S_1)=\Gamma_1,x:\Sigma$.
Výsledkom $generalize$ je celý rozšírený kontext, nie samotný typ ani schéma. Nová deklarácia $x$ nie je dostupná v $t_1$, keďže ide o nerekurzívnu let-väzbu.
Príklad
V prázdnom kontexte môžeme generalizovať jedinú typovú premennú identity:
$$generalize(\emptyset,\epsilon,id:\alpha\to\alpha)=\{id:\forall\alpha.\alpha\to\alpha\}.$$
Ak však $\Gamma=\{y:\alpha\}$, premenná $\alpha$ je voľná v kontexte. Pri prázdnej množine obmedzení teda dostaneme:
$$generalize(\emptyset,\Gamma,f:\alpha\to\beta)=\{y:\alpha,\ f:\forall\beta.\alpha\to\beta\}.$$
Generalizovali sme iba $\beta$. Typová premenná $\alpha$ musí zostať spoločná s typom $y$. Ak by aj $\beta$ bola voľná v kontexte, do novej deklarácie by sa nepridal žiadny kvantifikátor.
Inštanciácia
Definícia: Inštanciácia typovej schémy
Pre schému $\forall\alpha_1.\cdots\forall\alpha_n.S$ vytvorí $instantiate$ čerstvú monotypovú inštanciu:
$$instantiate(\forall\alpha_1.\cdots\forall\alpha_n.S)=[\alpha_1\mapsto\beta_1,\ldots,\alpha_n\mapsto\beta_n]S.$$
Premenné $\beta_1,\ldots,\beta_n$ sú navzájom rôzne a čerstvé pre celé aktuálne odvodenie. Každé volanie vyberá nové premenné; nejde o pevnú funkciu vždy vracajúcu tie isté mená. Voľné premenné schémy sa nemenia. Pre monotyp bez kvantifikátorov je výsledkom ten istý monotyp.
Príklad
Pre schému $\forall\alpha.\alpha\to\alpha$ môžu dve samostatné použitia vytvoriť:
$$instantiate(\forall\alpha.\alpha\to\alpha)=\beta\to\beta,\qquad instantiate(\forall\alpha.\alpha\to\alpha)=\gamma\to\gamma.$$
Čerstvé $\beta$ a $\gamma$ predstavujú nezávislé neznáme typy. Následná unifikácia ich môže určiť napríklad ako $\mathsf{Bool}$ a $\mathsf{Nat}$.
V každej inštanciácii zvoľ nové čerstvé typové premenné.
Pravidlá pre abstrakciu, aplikáciu, Bool a Nat preberáme zo siedmej prednášky s tým, že kontext teraz pripúšťa schémy a použitie premennej sa riadi CT-VarLet. Pre λ-viazaný parameter bez kvantifikátorov sa toto pravidlo zhoduje s pôvodným CT-Var.
Poznámka
Pracujeme s čistým nerekurzívnym HM. OCaml pridáva pri účinkoch obmedzenie na hodnoty a Haskell obsahuje okrem iného typové triedy; tieto rozšírenia nie sú súčasťou tu formalizovaného fragmentu.
Príklad
Aktualizácia existujúcich typových anotácií. Rekonštruujme predbežný typ a množinu obmedzení v zadaní:
$$\{y:\alpha\}\vdash\mathsf{let}\ x=\mathsf{succ}\ y\ \mathsf{in}\ \lambda z:\alpha.z:\ ?\mid\ ?$$
Označme zadaný kontext $\Gamma=\{y:\alpha\}$. Typová premenná $\alpha$ v kontexte a v anotácii parametra $z$ označuje tú istú zadanú neznámu; pri spracovaní ľavej vetvy ju už nevolíme nanovo.
1. Úplný strom prvej vetvy s obmedzeniami. Z kontextu prevezmeme typ $y$ a pravidlo CT-Succ pridá požiadavku, aby bol tento typ $\mathsf{Nat}$:
2. Unifikácia a aktualizácia kontextu. Pre prvú vetvu $t_1=\mathsf{succ}\ y$ sme získali:
$$S_1=\mathsf{Nat},\qquad C_1=\{\alpha=\mathsf{Nat}\},\qquad\sigma_1=[\alpha\mapsto\mathsf{Nat}].$$
Po aplikácii substitúcie je $\Gamma_1=\sigma_1(\Gamma)=\{y:\mathsf{Nat}\}$ a $U_1=\mathsf{Nat}$. Platí $FTV(U_1)\setminus FTV(\Gamma_1)=\emptyset$, preto nevznikne žiadny kvantifikátor. Kontext druhej vetvy označme:
$$\Gamma_2=generalize(C_1,\Gamma,x:S_1)=\{y:\mathsf{Nat},x:\mathsf{Nat}\}.$$
3. Aktualizácia anotácie a úplný strom druhej vetvy. Aktualizovať musíme aj existujúcu anotáciu v $t_2=\lambda z:\alpha.z$:
$$\sigma_1t_2=\sigma_1(\lambda z:\alpha.z)=\lambda z:\mathsf{Nat}.z.$$
Samotná aktualizácia kontextu by anotáciu v terme nezmenila. Pre telo abstrakcie označme $\Gamma_3=\Gamma_2,z:\mathsf{Nat}=\{y:\mathsf{Nat},x:\mathsf{Nat},z:\mathsf{Nat}\}$. Potom:
4. Úplný typovací strom celého let-termu s obmedzeniami. Pravá vetva typuje aktualizovaný term $\sigma_1t_2$. V závere CT-Let je pôvodný vstupný term a rovnosť $\alpha=\mathsf{Nat}$ zaznamenávajúca už vypočítanú substitúciu $\sigma_1$:
5. Výsledný typ a kontext. Druhá vetva dáva $S_2=\mathsf{Nat}\to\mathsf{Nat}$ a $C_2=\emptyset$, takže $\sigma_2=unify(C_2)=[\,]$. Celková substitúcia je $\sigma=\sigma_2\circ\sigma_1=[\alpha\mapsto\mathsf{Nat}]$ a výsledný typ je $\sigma_2(S_2)=\mathsf{Nat}\to\mathsf{Nat}$. Po aktualizácii kontextu aj anotácie dostaneme typovací úsudok:
$$\{y:\mathsf{Nat}\}\vdash\mathsf{let}\ x=\mathsf{succ}\ y\ \mathsf{in}\ \lambda z:\mathsf{Nat}.z:\mathsf{Nat}\to\mathsf{Nat}.$$
Substitúcia $\sigma_1t_2$ mení iba už prítomné typové anotácie. Ak $t_2$ žiadne anotácie neobsahuje, platí $\sigma_1t_2=t_2$.
Rozdiel medzi parametrom λ-abstrakcie a let-definíciou
V terme $\lambda f.t$ je $f$ parametrom funkcie. Všetky jeho výskyty v tele $t$ používajú jeden spoločný monotyp. Vo výraze $\mathsf{let}\ f=t_1\ \mathsf{in}\ t_2$ je $f$ meno definície, ktorej typ možno generalizovať; každý výskyt $f$ v $t_2$ potom môže mať nezávislú inštanciu tejto schémy. Parameter funkcie sa teda negeneralizuje tak ako let-definícia.
Príklad
V motivačnom príklade nebolo možné typovať
$$ (\lambda f.\mathsf{if}\ f\ \mathsf{true}\ \mathsf{then}\ f\ 5\ \mathsf{else}\ f\ 8)\;(\lambda x.x). $$
Ten istý výpočet zapíšeme ekvivalentným termom v tvare $\mathsf{let}$. Ide o výpočtovú ekvivalenciu: po dosadení definície identity dostaneme rovnaký podmienený výraz. Typovateľnosť v HM sa však zmení, pretože pri $\mathsf{let}$ môžeme typ identity generalizovať. Rekonštruujme typ tohto termu:
$$ \mathsf{let}\ id=\lambda x.x\ \mathsf{in}\ \mathsf{if}\ id\ \mathsf{true}\ \mathsf{then}\ id\ 5\ \mathsf{else}\ id\ 8. $$
1. Schéma typovacieho stromu. Najprv spracujeme definíciu identity. Označme $\Gamma_1=\{x:\alpha\}$; kontext druhej vetvy určíme až po generalizácii:
2. Typy a obmedzenia ľavej vetvy. Prvá vetva dá $S_1=\alpha\to\alpha$ a $C_1=\emptyset$:
Unifikácia prázdnej množiny dá $\sigma_1=[\,]$, preto $U_1=\sigma_1(S_1)=\alpha\to\alpha$ a aktualizovaný vonkajší kontext je stále prázdny.
3. Generalizácia. Premenná $\alpha$ nie je voľná vo vonkajšom kontexte, takže:
$$generalize(\emptyset,\epsilon,id:\alpha\to\alpha)=\Gamma_2=\{id:\forall\alpha.\alpha\to\alpha\}.$$
Schéma má funkčný typ $\alpha\to\alpha$, nie samotnú premennú $\alpha$. Po určení $\Gamma_2$ má rozpracovaný strom tvar:
4. Schéma pravej vetvy a inštanciácie. Tri použitia $id$ dostanú samostatné čerstvé premenné $\beta,\delta,\zeta$. Výsledky aplikácií označíme ďalšími čerstvými premennými $\gamma,\theta,\eta$:
5. Úplný typovací strom s obmedzeniami. Doplníme všetky monotypy a rovnosti. Podmienka CT-If vyžaduje booleovskú podmienku a zhodné typy oboch vetiev:
Odvodený predbežný typ celého termu je $\theta$. Keďže $C_1=\emptyset$ a $\sigma_1=[\,]$, množina rovností zaznamenávajúca $\sigma_1$ je prázdna a zostávajú iba obmedzenia pravej vetvy $C=C_2$:
$$ C=\left\{\beta\to\beta=\mathsf{Bool}\to\gamma,\ \delta\to\delta=\mathsf{Nat}\to\theta,\ \zeta\to\zeta=\mathsf{Nat}\to\eta,\ \gamma=\mathsf{Bool},\ \theta=\eta\right\}. $$
6. Unifikácia. Výpočet má dvanásť iterácií. V tabuľke je v každom riadku celá aktuálna množina obmedzení; stĺpec vpravo opisuje prechod na ďalší riadok.
| Iterácia | Množina obmedzení $C$ | Nasledujúca operácia |
|---|---|---|
| 1. | $\left\{\begin{array}{l}\beta \rightarrow \beta = \mathsf{Bool} \rightarrow \gamma,\ \delta \rightarrow \delta = \mathsf{Nat} \rightarrow \theta,\\\zeta \rightarrow \zeta = \mathsf{Nat} \rightarrow \eta,\ \gamma = \mathsf{Bool},\ \theta=\eta\end{array}\right\}$ | Rozklad prvej rovnosti funkčných typov. |
| 2. | $\left\{\begin{array}{l}\beta = \mathsf{Bool},\ \beta = \gamma,\\\delta \rightarrow \delta = \mathsf{Nat} \rightarrow \theta,\ \zeta \rightarrow \zeta = \mathsf{Nat} \rightarrow \eta,\\\gamma = \mathsf{Bool},\ \theta=\eta\end{array}\right\}$ | Eliminácia $[\beta\mapsto\mathsf{Bool}]$. |
| 3. | $\left\{\begin{array}{l}\mathsf{Bool} = \gamma,\ \delta \rightarrow \delta = \mathsf{Nat} \rightarrow \theta,\\\zeta \rightarrow \zeta = \mathsf{Nat} \rightarrow \eta,\ \gamma = \mathsf{Bool},\ \theta=\eta\end{array}\right\}$ | Eliminácia $[\gamma\mapsto\mathsf{Bool}]$. |
| 4. | $\left\{\begin{array}{l}\delta \rightarrow \delta = \mathsf{Nat} \rightarrow \theta,\ \zeta \rightarrow \zeta = \mathsf{Nat} \rightarrow \eta,\\\mathsf{Bool} = \mathsf{Bool},\ \theta=\eta\end{array}\right\}$ | Rozklad prvej rovnosti funkčných typov. |
| 5. | $\left\{\begin{array}{l}\delta = \mathsf{Nat},\ \delta = \theta,\\\zeta \rightarrow \zeta = \mathsf{Nat} \rightarrow \eta,\ \mathsf{Bool} = \mathsf{Bool},\ \theta=\eta\end{array}\right\}$ | Eliminácia $[\delta\mapsto\mathsf{Nat}]$. |
| 6. | $\left\{\begin{array}{l}\mathsf{Nat} = \theta,\ \zeta \rightarrow \zeta = \mathsf{Nat} \rightarrow \eta,\ \mathsf{Bool} = \mathsf{Bool},\\\theta=\eta\end{array}\right\}$ | Eliminácia $[\theta\mapsto\mathsf{Nat}]$. |
| 7. | $\{\zeta \rightarrow \zeta = \mathsf{Nat} \rightarrow \eta,\ \mathsf{Bool} = \mathsf{Bool},\ \mathsf{Nat}=\eta\}$ | Rozklad prvej rovnosti funkčných typov. |
| 8. | $\{\zeta = \mathsf{Nat},\ \zeta = \eta,\ \mathsf{Bool} = \mathsf{Bool},\ \mathsf{Nat}=\eta\}$ | Eliminácia $[\zeta\mapsto\mathsf{Nat}]$. |
| 9. | $\{\mathsf{Nat} = \eta,\ \mathsf{Bool} = \mathsf{Bool},\ \mathsf{Nat}=\eta\}$ | Eliminácia $[\eta\mapsto\mathsf{Nat}]$. |
| 10. | $\{\mathsf{Bool} = \mathsf{Bool},\ \mathsf{Nat}=\mathsf{Nat}\}$ | Odstránenie $\mathsf{Bool}=\mathsf{Bool}$. |
| 11. | $\{\mathsf{Nat}=\mathsf{Nat}\}$ | Odstránenie $\mathsf{Nat}=\mathsf{Nat}$. |
| 12. | $\{\}$ | Prázdna množina: návrat $[\,]$. |
Pri elimináciách sa substitúcie skladajú v poradí zodpovedajúcom algoritmu zo siedmej prednášky:
$$\begin{aligned} unify(C)&=[\,]\circ[\eta\mapsto\mathsf{Nat}]\circ[\zeta\mapsto\mathsf{Nat}]\circ[\theta\mapsto\mathsf{Nat}]\\ &\quad\circ[\delta\mapsto\mathsf{Nat}]\circ[\gamma\mapsto\mathsf{Bool}]\circ[\beta\mapsto\mathsf{Bool}]\\ &=\sigma_{mgu}. \end{aligned}$$
Po vyčíslení kompozície:
$$\sigma_{mgu}=[\beta\mapsto\mathsf{Bool},\gamma\mapsto\mathsf{Bool},\delta\mapsto\mathsf{Nat},\theta\mapsto\mathsf{Nat},\zeta\mapsto\mathsf{Nat},\eta\mapsto\mathsf{Nat}].$$
7. Výsledný typ. Aplikáciou na predbežný typ dostaneme:
$$\sigma_{mgu}(\theta)=\mathsf{Nat}.$$
V označení pravidla CT-Let je $\sigma_2=\sigma_{mgu}$ a celková substitúcia je $\sigma_2\circ\sigma_1=\sigma_{mgu}\circ[\,]=\sigma_{mgu}$.
Uzavretý term má typ $\mathsf{Nat}$. Voľba typov pre jednotlivé použitia identity prebehla nezávisle: prvá inštancia je booleovská, zvyšné dve číselné. V OCaml:
utop # let id=fun x -> x in if id true then id 5 else id 8;;
- : int = 5
OCamlovo $\mathtt{int}$ tu porovnávame s naším $\mathsf{Nat}$; OCaml pracuje so strojovými celými číslami aj so zápornými hodnotami.
Vlastnosti let-polymorfizmu
Pre skúmaný čistý Hindleyho–Milnerov systém s nerekurzívnou let-väzbou platia nasledujúce metateoretické vlastnosti. Ich úplné dôkazy nie sú súčasťou tejto prednášky; sústredíme sa na ich význam a súvislosť s typovou rekonštrukciou.
Vyhodnocujeme volaním hodnotou: vo výraze $\mathsf{let}\ x=t_1\ \mathsf{in}\ t_2$ najprv vyhodnotíme $t_1$ na hodnotu $v_1$ a potom pokračujeme termom $[x\mapsto v_1]t_2$. Dosadenie nezachytáva voľné premenné.
Zápis $\Gamma\vdash t:S$ tu označuje výsledné typovanie po vyriešení obmedzení, nie predbežný úsudok $\Gamma\vdash t:S\mid C$.
- Zachovanie typu (preservation): ak $\Gamma\vdash t:S$ a $t\to t'$, potom $\Gamma\vdash t':S$. Vyhodnocovanie vrátane dosadenia let-definície zachováva typ termu.
- Progres (progress): ak $\epsilon\vdash t:S$, term $t$ je hodnotou alebo môže vykonať ďalší krok. Uzavretý správne typovaný term sa nezasekne.
- Silná normalizácia: v tomto nerekurzívnom fragmente nemôže správne typovaný term vykonávať nekonečne veľa redukčných krokov. Vyhodnotenie uzavretého správne typovaného termu preto skončí hodnotou. Generalizácia a inštanciácia poskytujú polymorfizmus, nepridávajú mechanizmus všeobecnej rekurzie.
- Najvšeobecnejšie schémy a rozhodnuteľná rekonštrukcia: v klasickom systéme HM má každý typovateľný term najvšeobecnejšiu typovú schému vzhľadom na kontext a rekonštrukčný algoritmus skončí buď jej výpočtom, alebo odmietnutím termu.
Zachovanie typu a progres spolu vyjadrujú typovú bezpečnosť; normalizácia navyše zaručuje ukončenie. Tieto vlastnosti nemožno zamieňať. Po pridaní všeobecnej rekurzie môže jazyk zostať typovo bezpečný, hoci už pripúšťa nekonečné výpočty. Obmedzenie na nerekurzívny jazyk je preto pri tvrdení o normalizácii podstatné; tento rozdiel vysvetľuje aj výklad let-polymorfizmu a rekurzie.
Zhrnutie
Parametrický polymorfizmus umožňuje jednej definícii jednotne pracovať pri rôznych typoch. V Systéme F ho vyjadrujú typová abstrakcia $\Lambda\alpha.t$, univerzálny typ $\forall\alpha.T$ a typová aplikácia $t[U]$. Impredikatívnosť dovoľuje dosadiť za typový parameter aj polymorfný typ; preto možno typovať aj vhodne anotovanú sebaaplikáciu.
Typová kontrola plne explicitného Churchovského termu je rozhodnuteľná. V Curryho Systéme F je všeobecné hľadanie typov a chýbajúcich typových informácií nerozhodnuteľné. HM zachováva rozhodnuteľnosť pomocou prenexných schém a monotypových inštancií: pri let najprv vyrieši obmedzenia, generalizuje iba premenné nezávislé od kontextu a pri každom použití deklarácie vytvorí čerstvú inštanciu. λ-viazaný parameter zostáva monomorfný.
| Vlastnosť | Monomorfný STLC | Hindleyho–Milnerov systém | Systém F |
|---|---|---|---|
| Typové premenné | Neznáme typy pri rekonštrukcii | Neznáme monotypy a premenné viazané v schémach | Explicitné typové parametre v Churchovom štýle |
| Polymorfné typy alebo schémy | Nie | Prenexné schémy | Univerzálne kvantifikované typy |
| Nezávislé použitia jednej definície | Jedna väzba má jeden monotyp | Čerstvá inštancia let-schémy pri každom použití | Explicitné typové aplikácie |
| Kvantifikátor vo vstupe funkcie | Nie | Nie v monotypoch | Áno |
| Všeobecná rekonštrukcia z neanotovaného termu | Rozhodnuteľná | Rozhodnuteľná | V Curryho štýle nerozhodnuteľná |
| Kontrola úplného explicitného termu | Rozhodnuteľná | Kontrola voči zadanej schéme je rozhodnuteľná | V Churchovom štýle rozhodnuteľná |
Zdroje
- Benjamin C. Pierce: Types and Programming Languages. MIT Press, 2002, kapitoly 22 (Type Reconstruction) a 23 (Universal Types), najmä časť 23.6 o vymazaní typov a typovateľnosti.
- J. B. Wells: Typability and type checking in System F are equivalent and undecidable. Annals of Pure and Applied Logic 98, 1999, s. 111–156. Výsledok sa týka Curryho štýlu.
- Michael R. Clarkson et al.: OCaml Programming: Correct + Efficient + Beautiful – Type Inference, Cornell University. Najmä časti o let-polymorfizme, generalizácii a inštanciácii; priebežne aktualizovaný text.
- James Bornholt: Polymorphism and System F, University of Texas at Austin, jeseň 2022.
- Valerie Novitzká, Daniel Mihályi: Teória typov. TU Košice, 2015.