scientia

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

  Calculon

  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)

  • Idris

  5 názorů

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

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

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

  • Idris

  2 názory

• Intermezzo: Stručná historie teorie typů

  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.

  19. 9. 2018 21:26

  • Idris

• Jemný úvod do jazyka Idris (0)

  Calculon

  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)

  • Idris

  3 názory