Idris 0.9.15.1 released

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

The tutorial has also been updated.

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:

  • Naming of data and type constructors is made consistent across the standard library.
    • Note: This change will break existing code!
    • Data and Type Constructors now consistently begin with a capital letter, which means in particular we have Refl, FZ and FS for refl, fZ and fS.
    • The empty type is now called Void, and its eliminator void.
  • EXPERIMENTAL support for Uniqueness Types
  • EXPERIMENTAL support for Partial Evaluation, as described in Scrapping your Inefficient Engine.
  • The Java and LLVM backends have been factored out into separate projects, idris-java and idris-llvm.

There are several minor updates and improvements:

  • More efficient representation of the proof state, leading to faster elaboration of large expressions.
  • Two new tactics: skip and fail. skip does nothing, and fail takes a string as an argument and produces it as an error, with corresponding reflected tactics.
  • Improved display in the interactive prover.
  • Unary negation now desugars to `negate`, which is a method of the `Neg` type class. This allows instances of `Num` that can’t be negative, like `Nat`, and it makes correct IEEE Float operations easier to encode. Additionally, unary negation is now available to DSL authors.
  • New REPL command `:printdef` displays the internal definition of a name.
  • New REPL command `:pprint` pretty-prints a definition or term with LaTeX or HTML highlighting.
  • Terms in code blocks in documentation strings are now parsed and type checked. If this succeeds, they are rendered in full colour in documentation lookups, and with semantic highlighting for IDEs.
  • Fenced code blocks in docs defined with the “example” attribute are rendered as code examples.
  • Fenced code blocks declared to be Idris code that fail to parse or type check now provide error messages to IDE clients.