Idris (programovací jazyk)
programovací jazyk
Idris je čistě funkcionální programovací jazyk vyvinutý na Edinburské univerzitě. Jedná se o jazyk s formální verifikací v typovém systému, má proto induktivní a závislostní typy. Syntakticky vychází z jazyka Haskell.
Přirozená čísla se například v Idrisu definují takto:
data Nat : Type where
Z : Nat
S : Nat -> Nat
Tato definice vychází z Peanovy aritmetiky.
Jazyk obsahuje bohatou standardní knihovnu. Zdrojový kód se překládá do jazyka Scheme (dialektu Chez), existují ale další backendy, například C (s počítáním referencí), JavaScript, Java nebo Dart.