From the website (http://www.idris-lang.org/ http://www.idris-lang.org/): > Idris is a general purpose pure functional programming language with dependent type

From the website (http://www.idris-lang.org/ http://www.idris-lang.org/): > Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation.