Hlavní navigace

scientia

Jemný úvod do jazyka Idris (2) - Některé výrazy jsou si rovnější

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í.
11. 10. 2018 14:48 (aktualizováno)

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

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í.
5. 10. 2018 13:19 (aktualizováno)

Intermezzo: Stručná historie teorie typů

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.
19. 9. 2018 21:26

Jemný úvod do jazyka Idris (0)

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é…
5. 10. 2018 1:11 (aktualizováno)