Idris 0.9.19 released

A new version of Idris, 0.9.19, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. Updates are detailed below.

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.

Language changes

  • More flexible case construct, allowing each branch to target different types, provided that the case analysis does not affect the form of any variable used in the right hand side of the case.
  • decl syntax rules to allow syntax extensions at the declaration level
  • As usual, lots of improvements and fixes in elaboration

Library changes

  • The Show class has been moved into Prelude.Show and augmented with the method showPrec, which allows correct parenthesisation of showed terms. This comes with the type Prec of precedences and a few helper functions.
  • Use predicates instead of boolean equality proofs as preconditions on List functions
  • Moved System.Interactive, along with getArgs to the Prelude, in Prelude.Interactive.

Tool changes

  • New REPL command :printerdepth that sets the pretty-printer to only descend to some particular depth when printing. The default is set to a high number to make it less dangerous to experiment with infinite structures. Infinite depth can be set by calling :printerdepth with no argument.
  • Compiler output shows applications of >>= in do-notation
  • fromInteger i where i is an integer constant is now shown just as i in compiler output
  • An interactive shell, similar to the prover, for running reflected elaborator actions. Access it with :elab from the REPL.
  • Major improvements to reflected elaboration scripts, including the ability to run them in a declaration context and many bug fixes.
  • New command-line option --highlight that causes Idris to save highlighting information when successfully type checking. The information is in the same format sent by the IDE mode, and is saved in a file with the extension .idh.
  • Highlighting information is saved by the parser as well, allowing it to highlight keywords like case, of, let, and do
  • Some improvements in interactive editing, particularly in lifting out definitions and proof search. Proof search is now aware of type classes.
  • Experimental Windows support for console colours.

Other changes

Idris 0.9.18 released

A new version of Idris, 0.9.18, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. Updates are detailed below.

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.

Language changes

  • There is a new syntax for records, corresponding to type class syntax (which is also a record-like structure). See dependent records in the documentation
  • Records can now be coinductive, using the corecord keyword
  • Type class constructors can be given user accessible names (corresponding to the new record syntax)
  • if...then...else is now built in syntax rather than a syntax macro, desugaring to ifThenElse. This is for cleaner overloading and better error messages in domain specific languages.
  • Pattern matching lambdas and case expressions can now be labelled impossible, in
    the same way as top level patterns
  • Added a %hint function annotation, which allows functions to be used in proof search for auto arguments. Only functions which return instances of a data or record type are allowed as hints
  • Strings are now UTF8 encoded, and Idris source is assumed to be UTF8 encoded
  • Some reorganisation of primitives:
    • Buffer and BitVector removed (due to insufficient testing and lack of a maintainer)
    • Float renamed to Double
    • Externally defined primitives now supported with %extern directive
    • Ptr and ManagedPtr removed and replaced with external primitives
  • New quotation syntax `{n} for a quotation of the reflected representation of the name n. If n is lexically bound, then the resulting quotation will be for it, whereas if it is not, then it will succeed with a quotation of the unique global name that matches
  • As usual, lots of improvements and fixes in elaboration, especially with type class resolution
    and name disambiguation

Library changes

  • The default Semigroup and Monoid instances for Maybe are now prioritised choice, keeping the first success as Alternative does. The version that collects successes is now a named instance
  • The return types of Vect.findIndex, Vect.elemIndex and Vect.elemIndexBy were changed from Maybe Nat to Maybe (Fin n)

Tool changes

  • :exec REPL command now takes an optional expression to compile and run/show
  • A new :browse command shows the contents of a namespace
  • Agda-style semantic highlighting is supported over the IDE protocol