Types dépendants et programmation totale en Idris

Idris est un langage de programmation est un langage de programmation fonctionnelle disposant d'un système de types très expressif, entre autres grâce aux types dépendants. Ce mécanisme permet de faire dépendre les types de valeurs et ainsi de vérifier plus de propriétés lors de la compilation. L'exemple canonique est le type Vect, qui décrit à la fois le type des éléments et la longueur du vecteur. Ainsi l'opération d'inversion d'une liste garantit dans son type que la taille n'est pas affectée.

En complément de ce système de types, il est possible de prouver des propriétés mathématiquement sur son code, comme par exemple l'associativité ou la commutativité d'une opération. Idris fournit un assistant de preuve qui aide à démontrer une propriété pas à pas.

Idris peut s'exécuter sur différentes plateformes, en particulier LLVM et Javascript