Idris 0.9.10 released

A new version of Idris, 0.9.10, has been released. You can find this on hackage, or from the
download page, which contains a package for OS X and contains links to interactive editing modes for vim and emacs.

The tutorial has also been updated. The user visible changes are:

  • Type classes now implemented as dependent records, meaning that method types may now depend on earlier methods.
  • More flexible class instance resolution, so that function types and lambda expressions can be made instances of a type class.
  • Add !expr notation for implicit binding of intermediate results in monadic/do/etc expressions.
  • Extend Effects package to cope with possibly failing operations, using if_valid, if_error, etc.
  • At the REPL, it now refers to the previous expression.
  • Semantic colouring at the REPL. Turn this off with --nocolour.
  • Some prettifying of error messages.
  • The contents of ~/.idris/repl/init are run at REPL start-up.
  • The REPL stores a command history in ~/.idris/repl/history.
  • The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality checker and can thus be used in types. The [x..] syntax now returns an actually infinite stream.
  • Add %reflection option for functions, for compile-time operations on syntax.
  • Add expression form quoteGoal x by p in e which applies p to the expected expression type and binds the result to x in the scope e.
  • Performance improvements in Strings library.
  • Library reorganisation, separated into prelude and base.

There are several internal changes, mostly improving performance and fixing bugs:

  • New module/dependency tree checking.
  • New parser implementation with more precise errors.
  • Improved type class resolution.
  • Compiling Nat via GMP integers.
  • Performance improvements in elaboration.
  • Improvements in termination checking.
  • Various REPL commands to support interactive editing, and a client/server mode to allow external invocation of REPL commands.

Thanks, as ever, to everyone who has helped put this release together. You can find their names in the CONTRIBUTORS file in the source repository.

Being research software, 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