@hackage idris0.9.3

Functional Programming Language with Dependent Types

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 http://www.idris-lang.org/documentation. Features include:

  • Full dependent types with dependent pattern matching

  • where clauses, with rule, simple case expressions, pattern matching let and lambda bindings

  • Type classes, monad comprehensions

  • do notation, idiom brackets, syntactic conveniences for lists, tuples, dependent pairs

  • Indentation significant syntax, extensible syntax

  • Tactic based theorem proving (influenced by Coq)

  • Cumulative universes

  • Simple foreign function interface (to C)

  • Hugs style interactive environment