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.)
rewritecan now be used to rewrite equalities on functions over dependent types
rewritecan 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
usingnotation. 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
withsyntax, 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
| 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
%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.
%assert_total directive is now deprecated. Instead, you can use one of the functions
assert_unreachable to describe more precisely where a totality assertion is needed.
Control.WellFoundedmodule removed, and added to the Prelude as
Data.List.Viewswith views on
Listand their covering functions.
Data.Nat.Viewswith views on
Natand their covering functions.
Data.Primitives.Viewswith views on various primitive types and their covering functions.
System.Concurrency.Sessionsfor simple management of conversations between processes
- Taking cues from cabal, the
iPKGformat 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.
- 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-socket. These options were replaced with
- The code generator output type
MavenProjectwas specific to the Java codegen and has now been deprecated, together with the corresponding
- 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,
- The implicit coercion from String to TTName was removed.
- Decidable equality for TTName is available.