Idris (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.