Jan 17

Idris 0.9.0 released

Uncategorized Comments Off

A new version of Idris has been released on hackage. To install, run cabal update and type cabal install idris. To learn more, see the tutorial and FAQ.

This version is a complete rewrite. The user visible changes are:

• New proof/tactics syntax
• New syntax for pairs/dependent pairs
• Indentation-significant syntax
• Added type classes
• Added where clauses
• Added case expressions, pattern matching let and lambda
• Added monad comprehensions
• Added cumulativity and universe checking
• Ad-hoc name overloading, resolved by type or explicit namespace
• Modules (Haskell-style)
• public, abstract and private access to functions and types
• Improved interactive environment
• Replaced ‘do using’ with Monad class
• Extended syntax macros

The internal changes are:

• Everything . Most importantly, all definitions (functions, classes and instances) are now elaborated to a core language consisting of top level, fully explicit, data declarations and pattern matching definitions, which are verified by a minimal type checker.

This is the first release of a complete reimplementation. There will therefore, no doubt, be bugs. If you find any, please do not hesitate to contact Edwin Brady (ecb10 at st-andrews dot ac dot uk).