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
caseexpressions, pattern matching
letand lambda bindings
- Dependent records with projection and update
- Type classes
- Type-driven overloading resolution
donotation and idiom brackets
- Indentation significant syntax
- Extensible syntax
- Cumulative universes
- Totality checking
- Hugs style interactive environment
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
#idrison freenode. Point your irc client to
/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.
Many thanks to Heath Johns for designing the logo.