Hlavní navigace

Jemný úvod do jazyka Idris (1) - Konstrukce a eliminace

5. 10. 2018 13:19 (aktualizováno) Calculon

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

Vezměme si například zásadu tertium non datur, tedy zákon vyloučení třetího. Dokažme, že existují dvě iracionální čísla a a b taková, že ab je racionální. Položme pro začátek a=b=√2. Nevíme sice, jestli je √2√2 racionální, ale předpokládejme, že ano. Tím máme dokázáno. Pokud je ovšem √2√2 iracionální, můžeme uvažovat √2√2√2, což již zřejmě racionální je. Rozborem případů jsme ukázali, že existují dvě iracionální čísla a a b taková, že ab je racionální. V intuicionistické logice by nám ovšem takovýto důkaz neuznali, protože v ní neplatí, že každé tvrzení je buď pravdivé, nebo nepravdivé.

Podobně v intuicionistické logice neplatí ¬¬φ⊃φ, takže nemůžeme používat ani klasický důkaz sporem. Obecně platí, že intuicionistická logika je neslabší logikou, ve které platí modus ponens.

Vyhodnocování ve funkcionálních jazycích se dělá případnou eliminací výrazů a následnou normalizací hodnot. Každý datový typ poskytuje konstruktory pro vytváření hodnot (kromě typu Void, ke kterému se vrátíme později). Kupříkladu typ List má dva konstruktory: nulární Nil a binární ::. Platné hodnoty typu List jsou tedy třeba 1::Nil, 1::2::Nil nebo pouze Nil. Příkladem výrazu, který není hodnotou, je například head (1::2::Nil). Kontrolní otázka: Proč nejde o hodnotu? Symbol head v uvedeném výrazu je tzv. eliminátor. Základním pravidlem je, že zatímco konstruktory hodnoty tvoří (z jednodušších hodnot vytvářejí složitější), eliminátory naopak složité hodnoty rozebírají na jednodušší. Dalším příkladem budiž tail (1::2::Nil).

Kromě typů známých z běžných jazyků má Idris navíc rovnostní typy, =:a→bU, s jediným konstruktorem Refl. Rovnostní typ je obydlen (tj. má konstruktor) pouze v případě, že jsou oba jeho parametry (jež jsou hodnotami) shodné.

Sdílet