Idris es un lenguaje funcional de propósito general, con una particularidad es un lenguaje con Dependent type. Ahora viene la pregunta ¿que es Dependent type? Dependent type es un concepto de la programación pero también de la lógica; Dependent type es un tipo que depende de un valor. En la programación funcional se utiliza para prevenir errores, al permitir un sistema de tipo extensivo.
Dependent type añaden complejidad a un sistema de tipos. Es decir, para saber un tipo en algunos casos se deben realizar cálculos o ejecutar sentencias; esto hace bastante complejo el proceso de chequeo de tipos; y en algunos casos imposible. Pero algunos aspectos del comportamiento de un programa se pueden especificar con precisión en el tipo.
Idris es un lenguaje muy similar a haskell; pero con la propiedad de Dependent type.
Dejo links:
http://www.idris-lang.org/
