idris

Idris is a general purpose language with full dependent types. It is compiled, with eager evaluation. 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. The language is closely related to Epigram and Agda. There is a tutorial at http://www.idris-lang.org/documentation. Features include:

• Full dependent types with dependent pattern matching
• where clauses, with rule, simple case expressions, pattern matching let and lambda bindings
• Type classes, monad comprehensions
• do notation, idiom brackets, syntactic conveniences for lists, tuples, dependent pairs
• Totality checking
• Coinductive types
• Indentation significant syntax, extensible syntax
• Tactic based theorem proving (influenced by Coq)
• Cumulative universes
• Simple foreign function interface (to C)
• Hugs style interactive environment