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. Its features are influenced by Haskell and ML, and include:

• Full dependent types with dependent pattern matching
• Simple foreign function interface (to C)
• Compiler-supported interactive editing: the compiler helps you write code using the types
• where clauses, with rule, simple case expressions, pattern matching let and lambda bindings
• Dependent records with projection and update
• Type classes
• Type-driven overloading resolution
• do notation and idiom brackets
• Indentation significant syntax
• Extensible syntax
• Cumulative universes
• Totality checking
• Hugs style interactive environment

Getting Started

Tutorials and the beginnings of a manual are available on our documentation site.

Community

Mailing list

Long-form discussion happens on the mailing list.

IRC

There is also an irc channel #idris on freenode. Point your irc client to chat.freenode.net then /join #idris. Alternatively, there is a web interface.

GitHub

The Idris source is available from our repository. Tools and code by the wider Idris community are available in a GitHub organisation.

Idris development is led by Edwin Brady at the University of St Andrews.

Many thanks to Heath Johns for designing the logo.