A new version of Idris, 0.9.12, has been released. You can find this on hackage, or from the download page.

The tutorial has also been updated.

There are some changes in this release which may break old code, specifically laziness, codata and the effects library have been significantly updated. Full details are in the new tutorial, and in the Effects tutorial.

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.

Being research software, 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.

Details of the new feature and updates follow.

### Laziness

Laziness is now implemented via the type system, using the following constructs:

Lazy : Type -> Type
Delay : a -> Lazy a
Force : Lazy a -> a

Both `Delay`

and `Force`

may be left implicit, so laziness is usually silent apart from an explicit `Lazy`

in a type, e.g.

boolCase : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
boolCase True t e = t
boolCase False t e = e

### Codata

Similarly, codata is now implemented via the type system, using the following constructs:

Inf : Type -> Type
Delay : a -> Inf a
Force : Inf a -> a

Again, both `Delay`

and `Force`

may be left implicit. Data types may mix data and codata. Old style `codata`

declarations are still supported, where `Inf`

is added implicitly. The following declarations are therefore equivalent:

codata Stream : Type -> Type where
(::) : a -> Stream a -> Stream a
data Stream : Type -> Type where
(::) : a -> Inf (Stream a) -> Stream a

`Lazy`

and `Inf`

are closely related (in fact, the underlying implementation uses the same type). The only difference in practice is in totality checking, where `Lazy`

is erased (i.e. terms are checked for termination normally, ignoring laziness annotations), and `Inf`

uses a productivity checker, where any use of `Delay`

must be constructor guarded.

### Metavariables in types

Proof search now works for metavariables in types, giving some interactive type inference. For example:

vec : ?vtype
vec = with Vect ["a","b","c"]

This can either be solved interactively, using `:ps`

at the REPL, or the appropriate vim mode or emacs mode commands. e.g. assuming it is defined on line 37 of `vtest.idr`

:

*vtest> :ps 37 vtype
Vect 3 String

Alternatively, it can be solved explicitly in code:

vec : ?vtype
vec = with Vect ["a","b","c"]
vtype = proof search

### Documentation comments

There is a new syntax for inline documentation. Documentation starts with |||, and

arguments are documented by preceding their name with @. For example:

||| Add two natural numbers
||| @ n the first number (examined by the function)
||| @ m the second number (not examined)
plus (n, m : Nat) -> Nat

### Other changes

There have been several improvements in robustness and efficiency. Other changes are:

- JavaScript and Node codegen now understand the
`%include`

directive.
- Concept of
`null`

is now understood in the JavaScript and Node codegen.
- Lots of performance patches for generated JavaScript.
- New commands
`:eval`

(`:e`

) and `:type`

(`:t`

) in the prover, which either normalise or show the type of expressions.
- Allow type providers to return postulates in addition to terms.
- Syntax for dealing with match failure in
`<-`

and pattern matching `let`

.
- Allow the auto-solve behaviour in the prover to be disabled, for easier debugging of proof automation. Use
`:set autosolve`

and `:unset autosolve`

.
- Updated
`effects`

library.
- New
`:apropos`

command at REPL to search documentation, names, and types.
- Unification errors are now slightly more informative.
- Add
`covering`

function option, which checks whether a function and all descendants cover all possible inputs (subset of `total`

).