Oct 29

Idris 0.9.5 released

Uncategorized Add Comment (0)

Idris version 0.9.5 has been released on Hackage. To install, run cabal update and type cabal install idris. This release includes a new termination checker, coinduction, much improved compilation and code generation through more aggressive erasure and inlining, as well as several minor additions and fixes.

It includes the following user visible changes:

• Added codata declarations
  • as data declarations, but constructor arguments are evaluated lazily
  • functions which return a codata type do not reduce at compile time
• New termination checker supporting mutually recursive definitions.
• Added parameters blocks
• Allow local data definitions in where blocks
• Added %default directive to declare total-by-default or partial-by-default for functions, and a corresponding partial reserved word to mark functions which are allowed to be partial.
• Command line options --total and --partial to declare total or partial by default.
• Command line option --warnpartial for flagging all undeclared partial functions, without error.
• Added :load command to REPL, for loading a new file
• Added :module command to REPL, for adding modules
• Renamed library modules (now have initial capital)

The internal changes are:

• Added collapsing optimisation and more aggressive erasure
• Several improvements and fixes to unification

Thanks to everyone who has helped put this release together.

As always, please report any problems on the github issue tracker. Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.