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.


Mailing list
Long-form discussion happens on the mailing list.
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.
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.