Idris 0.9.17 released

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

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

The main new features and updates are:

  • Library operators have been renamed for consistency with corresponding operators in Haskell. In particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is now an alias for Correspondingly, ($>) and (<$) have been renamed to (<*) and (*>). The cascading effects of this rename are that Algebra.(<*>) has been renamed to Algebra.(<.>) and Matrix.(<.>) is now Matrix.(<:>).
  • Types errors have been improved, now giving the provenance of incorrect types
  • Documentation has been updated and moved to, hosted by Read the Docs.
  • Web documentation is now available for packages, from the Documentation page.
  • A new package contrib has been added to the libraries. This is for things which are less mature or less used than the contents of base.contrib is not available by default, so you may need to add -p contrib to your .ipkg file or Idris command line.
  • Instances and type providers can now be given documentation strings.
  • Lots of issues relating to type class resolution have been resolved. In particular:
    • Arguments are now checked for injectivity, since this is assumed throughout unification
    • Multi-parameter type classes can now be given determining parameters, which are the parameters used to resolve class instances. Only determining parameters are assumed and checked to be injective.
  • Binding forms in dsl notation are now given an extra argument: a reflected representation of the name that the user chose. Specifically, the rewritten lambda, pi, and let binders will now get an extra argument of type TTName. This allows more understandable dynamic errors in DSL code and more readable code generation results.
  • The Foreign Function Interface has been updated to support multiple back end descriptions.
  • A new FFI_Export type has been added, supporting export of functions to be called by foreign code. Details of the FFI and its interaction with back ends are given in this draft paper.