Idris is a general purpose language with full dependent types. It is compiled,
with eager evaluation. 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. The language is closely related to Epigram and Agda.
There is a tutorial at www.idris-lang.org/documentation.
* Full, first class, dependent types with dependent pattern matching
* where clauses, with rule, case expressions, pattern matching let and
* Interfaces (similar to type classes), monad comprehensions
* do notation, idiom brackets, syntactic conveniences for lists, tuples,
* Totality checking
* Coinductive types
* Indentation significant syntax, extensible syntax
* Cumulative universes
* Simple foreign function interface (to C)
* Hugs style interactive environment.