scientia

V minulém díle jsme si řekli, že v Idrisu jsou kromě „běžných“ typů také typy rovnostní, jejichž (generickou) definici si můžeme představit zhruba takto: /---pre data (=) : a → b → Type where Refl : x = x \--- Konstruktor je nanejvýš jeden, a to pouze v případě, že se oba argumenty shodují. To dává smysl, připomeňte si, že typy odpovídají logickým výrokům, takže existence konstruktoru znamená, že výrok platí.

Jak je v IT všeobecně známo, typové systémy žijí dvojím životem. Na jednu stranu se tváří jako množiny a operaci nad nimi jako běžné programy, ale na stranu druhou odpovídají typy logickým tvrzením a jejich prvky důkazům. Příslušná symbolická logika není ovšem logikou známou z matematiky. Jde o tzv. logiku intuicionistickou, ve které mnohá tvrzení považovaná za samozřejmá neplatí.

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.

Jazyk Idris byl navržen pro ty, jimž Haskell připadá málo abstraktní. Snad vás tato věta neodradí, nepřestanete číst a dozvíte se něco nového a užitečného. Idris je jazyk funkcionální, což znamená, že je založen na λ-kalkulu, konkrétně typovaném λ-kalkulu (TλK). Ten má několik zajímavých vlastností: 1) Je turingovsky úplný, tj. jde v něm naprogramovat vše, co je vyčíslitelné…