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
• Interfaces (similar to type classes in Haskell)
• 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.

All participants in these forums are requested to abide by the community standards.

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

Many thanks to Heath Johns for designing the logo.