Overview

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
  • where clauses, with rule, simple case expressions, pattern matching let and lambda bindings
  • Dependent records with projection and update
  • Type classes
  • Monad comprehensions
  • Syntactic conveniences for lists, tuples, dependent pairs
  • do notation and idiom brackets
  • Indentation significant syntax
  • Extensible syntax
  • Tactic based theorem proving (influenced by Coq)
  • Cumulative universes
  • Totality checking
  • Simple foreign function interface (to C)
  • Hugs style interactive environment

There is a mailing list and a tutorial. You can also see a simple example.

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.

Contact

Idris is mainly developed by Edwin Brady at the University of St Andrews.

Related searches:
dependent simple released tutorial syntax
gipoco.com is neither affiliated with the authors of this page nor responsible for its contents. This is a safe-cache copy of the original web site.