Hlavní navigace

Jemný úvod do jazyka Idris (1)

2. 4. 2018 15:52 (aktualizováno) 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é. 2) Jde do něj “vnořit” logika vyššího řádu (“vnoření” je matematický pojem znamenající, že v něm jde “nasimulovat” se vším všudy). 3) Má úplnou sémantiku, tj. každá platná formule je dokazatelná. Tímto jsme si odbyli teorii a můžeme se vrhnout na záživnější věci.

Idris se překládá do C (a také Javascriptu), takže svůj program pustíte prakticky všude. Hlavní výhodou Idrisu je podpora závislostních typů—závisejících na nějakých konkrétních hodnotách. To je podstatný rozdíl oproti běžným jazykům, kde tzv. generické typy závisí pouze na jiných typech, nikoliv hodnotách. Nejjednodušším příkladem je pole pevné délky—vector[N], kde N je kladné celé číslo. Tento typ má michochodem například i Go, je to ovšem jediný závislostní typ, na který tam narazíte. Idris umožňuje tvorbu vlastních.

Idris stojí a padá kromě λ-kalkulu s teorií typů. Tu původně vymyslel velšský filosof Bertrand Russell, aby se zbavil paradoxů v Cantorově naivní teorii množin. Do IT ji zavedl Church spářením s původně netypovaným λ-kalkulem, čímž vznikla směska, jež se záhy a k údivu všech zasvěcených ukázala být univerzálním výpočetním nástrojem na pomezí informatiky a formální logiky.

Typy jsou něco jako jednotky ve fyzice, které znáte ze základní školy. Chci-li sečíst dvě hodnoty, musí mít stejný typ, tedy jednotky. Můžu tedy kupříkladu sečíst dvě rychlosti mající “typ” m s-1, ale ne třeba rychlost a hmotnost. Podobně to je i s typy v Idrisu, jen na podstatně složitější úrovni.

Abstraktní typ si lze nejjednodušeji představit jako množinu nějakých hodnot, například čísel, textových řetězců nebo kombinací hodnot jiných typů. Existují dva typy těchto “kombinací”, tzv. součinové a součtové. Mějme například výčtový typ T nabývající hodnot {1,2,3,4,5}. Dále mějme typ U s hodnotami {A,B,C}. Nyní můžeme nadefinovat součinový typ T×U skládající se z dvojic hodnot typu T a U. Celkem má 5 krát 3 = 15 hodnot, proto součinový. Podobně můžeme nadefinovat součtový typ T+U mající 8 hodnot, buď z T nebo z U.

A nakonec, aby tu nebyl jen text, uveďme alespoň obligátní „hello world“:

module Main

main : IO ()
main = putStrLn "Hello, world!"

Tento “nultý” díl je tak trochu sonda, směr dá tomuto seriálu diskuse pod tímto článkem. Má hrubá představa je projít syntax od funkcí vyšších řádů přes generické typy po typy závislostní—za použití příkladů a bez zabředávání do teorie, pokud si o ni výslovně neřeknete. Předpokládaná délka seriálu je cca. 5 dílů, nicméně v případě zájmu se určitě najdou témata k pokračování.