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 is now implemented via the type system, using the following constructs:
Lazy : Type -> Type Delay : a -> Lazy a Force : Lazy a -> a
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
Similarly, codata is now implemented via the type system, using the following constructs:
Inf : Type -> Type Delay : a -> Inf a Force : Inf a -> a
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
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> :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
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
There have been several improvements in robustness and efficiency. Other changes are:
- Concept of
- New commands
: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
- Allow the auto-solve behaviour in the prover to be disabled, for easier debugging of proof automation. Use
:aproposcommand at REPL to search documentation, names, and types.
- Unification errors are now slightly more informative.
coveringfunction option, which checks whether a function and all descendants cover all possible inputs (subset of