idris: 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

Downloads

• idris-0.9.2.tar.gz [browse] (Cabal source package)
• Package description (as included in the package)

Maintainer's Corner

Package maintainers

• EdwinBrady, niklasl

For package maintainers and hackage trustees

• edit package information

Candidates

• 0.9.9.3, 0.9.10, 0.9.17, 0.9.17.1, 0.9.18, 0.9.18.1, 0.9.19, 0.9.19.1, 0.9.20, 0.9.20.1, 0.10, 0.10.1, 0.10.2, 0.10.3, 0.11, 0.11.2, 0.12, 0.12.2, 0.12.3, 0.99, 0.99.1, 0.99.2, 1.0, 1.0.1, 1.1.0, 1.1.1, 1.2.0, 1.3.0, 1.3.1, 1.3.2