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

• Totality checking

• Coinductive types

• Indentation significant syntax, extensible syntax

• Tactic based theorem proving (influenced by Coq)

• Cumulative universes

• Simple foreign function interface (to C)

• Hugs style interactive environment

Modules

[Last Documentation]

Flags

Manual Flags

Name	Description	Default
llvm	Build the LLVM backend	Disabled
ffi	Build support for libffi	Disabled
gmp	Use GMP for Integers	Disabled
curses	Use Curses to get the screen width	Disabled
release	This is an official release	Enabled
freestanding	Build an Idris that doesn't use cabal	Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

• idris-0.9.14.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