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é…