Idris 0.99.1 Released

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

This release mostly contains bug fixes and minor improvements, aiming towards releasing version 1.0 around the same time as the publication of Type Driven Development with Idris which will be very soon. There is also a new experimental feature, working towards support for linear types, but don’t expect this to work properly yet :). The changes since version 0.99 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.

Language updates

  • Language pragmas are now required for the less stable existing features, in addition to the existing TypeProviders and ErrorReflection:
    • ElabReflection, which must be enabled to use %runElab
    • UniquenessTypes, which must be enabled to use UniqueType
    • DSLNotation, which must be enabled to define a dsl block
    • FirstClassReflection, which must be enabled to define a %reflection function
  • New language extension LinearTypes:
    • This allows adding a /multiplicity/ to a binder which says how often it is allowed to be used; either 0 or 1 (if unstated, multiplicity is “many”)
    • The typing rules follow Conor McBride’s paper “I Got Plenty o’ Nuttin'”
    • This is highly experimental, unfinished, not at all polished. and there are still lots of details to sort out. Some features don’t quite work properly yet. But it is there to play with for the brave!

Library Updates

  • Terminating programs has been improved with more appropriate functions (exitWith, exitFailure, and exitSuccess) and a data structure (ExitCode) to capture a program’s return code.
  • Casting a String to an Int, Integer or a Double now ignores leading and trailing whitespace. Previously only leading whitespace was ignored.
  • RTS functions openFile, do_popen, and ARGV are now properly encoded using UTF-8 on Windows.
  • New module Control.ST in contrib for implementing and combining state transition systems

Tool Updates

  • Idris’ output has been updated to more accurately reflect its progress through the compiler i.e. Type Checking; Totality Checking; IBC Generation; Compiling; and Code Generation. To control the loudness of the reporting three verbosity levels are introduced: --V0, --V1, and --V2. The old aliases of -V and --verbose persist.
  • New REPL command :! that runs an external shell command.
  • The REPL now colourises output on MinTTY consoles (e.g., Cygwin and MSYS) on Windows, which previously did not occur due to a bug.
  • Idris now runs in a UTF-8-compatible codepage on Windows. This fixes many Unicode-rendering issues on Windows (e.g., error messages stating commitBuffer: invalid argument (invalid character)).
  • Idris now has a --warnipkg flag to enable auditing of Idris packages during build time. Currently auditing check’s the list of modules specified in the iPKG file with those presented in the package directory.