Hlavní navigace

Intermezzo: Stručná historie teorie typů

19. 9. 2018 21:26 Calculon

Teorie typů začala svou existenci jako prostředek k formalizaci Cantorovy teorie množin. Její první verzi vymyslel velšský filosof a matematik Bertrand Russel poté, co v teorii množin objevil logické paradoxy vedoucí ke sporu, což se matematikům většinou moc nelíbí. Zavedl základní pojmy jako typ a úsudek (například 3:ω, tj. typem čísla 3 jsou přirozená čísla). V době svého vzniku vyvolala rozporuplné reakce a zpočátku se příliš neujala.

Impuls dal teorii typů Alonso Church, který ji spojil s λ-počtem, čímž vznikla tzv. jednoduchá teorie typů. V této teorii má každá hodnota (a proměnná) pevně určený typ. V původní verzi existují dva základní typy—ι pro individua a ο pro pravdivostní hodnoty—a jeden jediný typový operátorkonkatenace (jsou-li α a β typy, je také αβ typ, interpretovaný jako funkce z β do α). Leon Henkin, který se proslavil zejména jednodušším (oproti Gödelovu) důkazem úplnosti predikátové logiky, dokázal, že Churchova teorie typů má úplnou sémantiku, z čehož přímo plyne, že logika druhého (a jakéhokoliv vyššího) řádu má úplnou sémantiku, neboť ji lze do Churchovy teorie vložit (připomeňme, že logický systém je úplný, je-li každý platný výrok dokazatelný). Henkinův důkaz je konstruktivní, iterativně se sestrojuje model pro libovolnou bezespornou teorii. Zajímavé rovněž je, že takto sestrojený model je vždy spočetný. V Churchově teorii typů mají logické výrazy typ ο, predikáty mají typ οι apod.

Matematik Haskell Brooks Curry a nezávisle na něm logik William Alvin Howard (student Saunderse Mac Lana, jednoho ze zakladatelů teorie kategorií) si všimli, že typy přímo odpovídají výrokům ve formální logice, přičemž termy lze interpretovat jako důkazy. Tuto korespondenci záhy rozvinul filosof Per Martin-Löf do své intuicionistické teorie typů, jež se později stala základem pro řadu jazyků s velmi silným typovým systémem, ve kterém lze vyjádřit jakoukoliv vyčíslitelnou funkci (dokazatelnost v této logice splývá s vyčíslitelností). Rozšíření spočívalo v přidání zvláštních typů pro kvantifikátory a hlavně pro rovnost—zvláštní polymorfní typový operátor IdA se signaturou AAU vytváří typ rovnosti. Místo IdA(a,b) se někdy píše přímo a=Ab (typový operátor = si nepleťte s ekvivalencí). Pokud rovnost platí, typ a=Ab je takzvaně obydlený (inhabited), v opačném případě je neobydlený (uninhabited), což znamená, že nelze sestrojit důkaz rovnosti. V nejjednodušší verzi intuicionistické teorie typů mají obydlené typy rovnosti konstruktor refl:a=Aa.

Ve složitějších verzích teorie typů s rovností se typy interpretují jako topologické prostory a termy jako body v nich. Rovnost je pak cesta mezi body a posuneme-li se o úroveň výše, můžeme zkoumat i rovnost rovnosti, tedy cest, čímž se dostaneme k topologické homotopii, na níž je založená tzv. homotopická teorie typů. Tu asi ale nechme na jindy.

K čemu je to všechno dobré? Představme si, že máme funkci nad přirozenými čísly (tedy se signaturou ωω) a chceme pokud možno zaručit její korektnost. V „běžném“ jazyce bychom napsali pár jednotkových testů a doufali v dostatečné pokrytí. V jazyce s dostatečně silným (intuicionistickým) typovým systémem bychom ale mohli korektnost testovat ještě před spouštěním kódu (tedy v době překladu). Pro funkci f vytvoříme funkci fProof, jejíž typ bude navržen tak, aby vypočtená hodnota jednoznačně potvrdila korektnost implementace. Její signatura bude n:ωn=ωfCheck(n). Je to k nevíře, ale typová kontrola překladače symbolicky překontroluje, že výsledek je správně (připomeňme, že typy přímo odpovídají logickým výrokům). V nejjednodušším případě by definicí funkce bylo prostě f(n)=refl, mnohé překladače umí automaticky odvodit i značně složité důkazy. Ve složitějších případech bychom museli překladači pomoci, ale o tom někdy jindy.

Sdílet