Idris 0.12 Released

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

(Note: If you are installing from source, Idris 0.12 does not currently build with GHC 8.0.1 due to dependency issues. There’ll be a patch release once this issue is resolved.)

Language updates

  • rewrite can now be used to rewrite equalities on functions over dependent types
  • rewrite can now be given an optional rewriting lemma, with the syntax rewrite [rule] using [rewrite_lemma] in [scope].
  • Reorganised elaboration of implementation, so that interfaces with dependencies between methods now work more smoothly
  • Allow naming of parent implementations when defining an implementation. For example:
[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

-- use PlusNatSemi as the parent implementation
[PlusNatMonoid] Monoid Nat using PlusNatSemi where
  neutral = 0

-- use MultNatSemi as the parent implementation
[MultNatMonoid] Monoid Nat using MultNatSemi where
  neutral = 1
  • Interface definitions can now include data declarations (but not data definitions). Any implementation of the interface must define the method using a data type. The effect is to cause Idris to treat the method as a data type (for unification and interface resolution purposes).
  • Experimentally, allow named implementations to be available by default in a block of declarations with using notation. For example:
using implementation PlusNatMonoid
  test : Nat -> Nat
  test x = x <+> x <+> neutral
  • Constraint arguments can now appear anywhere in function types, not just at the top level or after an implicit argument binding.
  • Experimental extended with syntax, which allows calling functions defined in a with block directly. For example:
data SnocList : List a -> Type where
     Empty : SnocList []
     Snoc : SnocList xs -> SnocList (xs ++ [x])

snocList : (xs : List a) -> SnocList xs

my_reverse : List a -> List a
my_reverse xs with (snocList xs)
  my_reverse [] | Empty = []
  my_reverse (ys ++ [x]) | (Snoc p) = x :: my_reverse ys | p

The | p on the right hand side means that the with block function will be called directly, so the recursive structure of SnocList can direct the recursion structure of my_reverse.
* Added %fragile directive, which gives a warning and a message when a fragile name is referenced. For use in detailing fragile APIs.
* The totality checker now looks under case blocks, rather than treating them as mutually defined functions with their top level function, meaning that it can spot more total functions.
* The totality checker now looks under if...then...else blocks when checking for productivity.
* The %assert_total directive is now deprecated. Instead, you can use one of the functions assert_total, assert_smaller or assert_unreachable to describe more precisely where a totality assertion is needed.

Library updates

  • Control.WellFounded module removed, and added to the Prelude as Prelude.WellFounded.
  • Added Data.List.Views with views on List and their covering functions.
  • Added Data.Nat.Views with views on Nat and their covering functions.
  • Added Data.Primitives.Views with views on various primitive types and their covering functions.
  • Added System.Concurrency.Sessions for simple management of conversations between processes

iPKG Updates

  • Taking cues from cabal, the iPKG format has been extended to include more package metadata information. The following fields have been added:
    • brief: Brief description of the package.
    • version: Version string to associate with the package.
    • readme: Location of the README file.
    • license: Description of the licensing information.
    • author: Author information.
    • maintainer: Maintainer information.
    • homepage: Website associated with the package.
    • sourcepage: Location of the DVCS where the source can be found.

Miscellaneous updates

  • The Idris man page is now installed as part of the cabal/stack build process.
  • Improved startup performance by reducing the processing of an already imported module that has changed accessibility.
  • A limited set of command line options can be used to override package declared options. Overridable options are currently, logging level and categories, default totality check, warn reach, IBC output folder, and idris path. Note overriding IBC output folder, only affects the installation of Idris packages.
  • Remove deprecated options --ideslave and --ideslave-socket. These options were replaced with --ide-mode and --ide-mode-socket in 0.9.17
  • The code generator output type MavenProject was specific to the Java codegen and has now been deprecated, together with the corresponding --mvn option.
  • Definitional equality on Double is now bit-pattern identity rather than IEEE’s comparison operator. This prevents a bug where programs could distinguish between -0.0 and 0.0, but the type theory could not, leading to a contradiction. The new fine-grained equality prevents this.
  • Naming conventions for Idris packages in an iPKG file now follow the same rules for executables. Unquoted names must be valid namespaced Idris identifiers e.g. package my.first.package. Quoted package names allow for packages to be given valid file names, for example, package "my-first-package".

Reflection changes

  • The implicit coercion from String to TTName was removed.
  • Decidable equality for TTName is available.