Idris 1.1.0 released

A new version of Idris, 1.1.0, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. Details of the changes since version 1.0 are listed 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.

Library Updates

  • Added Text.Lexer and Text.Parser to contrib. These are small libraries for implementing total lexical analysers and parsers.
  • Added Text.PrettyPrint.WL an implementation of the Wadler-Leijen Pretty-Print algorithm.
  • New instances:
    • Added Catchable for ReaderT, WriterT, and RWST.
    • Added MonadTrans for RWST.
  • Added utility functions to Data.SortedMap and Data.SortedSet (contrib), most notably merge, merging two maps by their Semigroup op (<+>)
  • Prelude.WellFounded now contains an interface Sized a that defines a size mapping from a to Nat. For example, there is an implementation for lists, where size = length.

    The function sizeAccessible then proves well-foundedness of the relation Smaller x y = LT (size x) (size y), which allows us to use strong induction conveniently with any type that implements Sized.

    In practice, this allows us to write functions that recurse not only on direct subterms of their arguments but on any value with a (strictly) smaller size.

    A good example of this idiom at work is Data.List.Views.splitRec from base.

  • Added utility lemma decEqSelfIsYes : decEq x x = Yes Refl to Decidable.Equality. This is primarily useful for proving properties of functions defined with the help of decEq.

Tool Updates

  • New JavaScript code generator that uses an higher level intermediate representation.
  • Various optimizations of the new JavaScript code generator.
  • Names are now annotated with their representations over the IDE protocol, which allows IDEs to provide commands that work on special names that don’t have syntax, such as case block names.