Idris 0.9.14 released

A new version of Idris, 0.9.14, has been released. You can find this on hackage, or from the download page.

The tutorial has also been updated.

This release is primarily to improve robustness and efficiency, and solves several long-standing issues. There is also a new, improved, JavaScript backend and better syntactic support for reflection.

Thanks as always to everyone who has contributed, either with code, documentation or by testing and reporting issues. You can find the names of all contributors in the CONTRIBUTORS file in the source repository.

Idris is still research software, so we expect there to be bugs. Please don’t keep them to yourself! If you find any problem, please report it on the github issue tracker. It is very helpful if you can also provide a small test case which reproduces your problem.

Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.

The main new features and updates are:

  • Tactic for case analysis in proofs
  • Induction and case tactic now work on expressions
  • Support for running tests for a package with the tests section of .ipkg files and the --testpkg command-line option
  • Clearly distinguish between type providers and postulate providers at the use site
  • Allow dependent function syntax to be overridden in dsl blocks, similarly to functions and let. The keyword for this is pi.
  • Updated effects library, with simplified API
  • All new JavaScript backend (avoids callstack overflows)
  • Add support for %lib directive for NodeJS
  • Quasiquotes and quasiquote patterns allow easier work with reflected terms.`(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected version of it. Subterms prefixed with ~ are unquoted – on the RHS, they are reflected terms to splice in, while on the LHS they are patterns. A quasiquote expression can be given a goal type for the elaborator, which helps with disambiguation. For instance, `(() : ()) quotes the unit constructor, while `(() : Type) quotes the unit type. Both goal types and quasiquote are typechecked in the global environment.
  • Better inference of unbound implicits.