Idris 0.9.13 released

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

The tutorial has also been updated.

This release primarily improves robustness and efficiency, and more in-depth documentation. In particular, there is a new implementation of erasure by usage analysis.

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.

Aside from erasure, the new features and updates are:

  • New (first class) nested record update/access syntax:
    • record { a->b->c = val } x sets field accessed by c (b (a x)) to val
    • record { a->b->c } x accesses field, equivalent to c (b (a x))
  • IDE support for retrieving structured information about metavariables
  • Experimental Bits support for JavaScript
  • IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
  • Command line option -e (or --eval) to evaluate expressions without loading the REPL. This is useful for writing more portable tests.
  • Many more of the basic functions and datatypes are documented
  • Primitive types such as Int and String are documented
  • Removed javascript lib in favor of idris-hackers/iQuery
  • Specify codegen for :compile REPL command (e.g. :compile javascript program.js)
  • Remove :info REPL command, subsume and enhance its functionality in the :doc command.
  • The banner at startup can be suppressed by adding :set nobanner to the initialisation script.
  • :apropos now accepts space-delimited lists of query items, and searches for the conjunction of its inputs. It also accepts binder syntax as search strings – for instance, -> finds functions.
  • Totality errors are now treated as warnings until code generation time, when they become errors again. This allows users to use the interactive editing features to fix totality issues, but no programs that violate the stated assumptions will actually run.
  • Added :makelemma command, which adds a new top level definition to solve a metavariable.
  • Extend :addclause to add instance bodies as well as definitions
  • Reverse parameters to BoundedList — now matches Vect, and is easier to instantiate classes.
  • Move foldl into Foldable so it can be overridden.
  • Experimental :search REPL command for finding functions by type

Idris 0.9.12 released

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).

Idris 0.9.11.1 released

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

The tutorial has also been updated.

This release mostly improves robustness and efficiency. The user visible changes are:

  • Agda-style equational reasoning (in Syntax.PreorderReasoning)
  • case construct now abstracts over the scrutinee in its type
  • Added label type 'name (equivalent to the empty type). This is intended for field/effect disambiguation. name can be any valid identifier. Two labels are definitionally equal if they have the same name.
  • General improvements in error messages, especially %error_reverse annotation, which allows a hint as to how to display a term in error messages
  • --ideslave mode now transmits semantic information about many of the strings that it emits, which can be used by clients to implement semantic highlighting like that of the REPL. This has been implemented in the Emacs mode and the IRC bot, which can serve as examples.
  • New expression form: with [name] [expr] privileges the namespace name when disambiguating overloaded names. For example, it is possible to write with Vect [1,2,3] at the REPL instead of the (Vect _ _) [1,2,3], because the Vect constructors are defined in a namespace called Vect.
  • assert_smaller internal function, which marks an expression as smaller than a pattern for use in totality checking. e.g. assert_smaller (x :: xs) (f xs) asserts that f xs will always be structurally smaller than (x :: xs).
  • assert_total internal function, which marks a subexpression as assumed to be total, e.g assert_total (tail (x :: xs)).
  • Terminal width is automatically detected if Idris is compiled with curses support. If curses is not available, automatic mode assumes 80 columns.
  • Changed argument order for Prelude.Either.either.
  • Experimental neweffects library, intended to replace effects in the next release.

Internal changes are:

  • Faster parsing and elaboration
  • Smaller .ibc files
  • Pretty-printer now used for all term output

Thanks, as ever, to everyone who has helped put this release together. You can find their names 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.

Idris 0.9.10 released

A new version of Idris, 0.9.10, has been released. You can find this on hackage, or from the
download page, which contains a package for OS X and contains links to interactive editing modes for vim and emacs.

The tutorial has also been updated. The user visible changes are:

  • Type classes now implemented as dependent records, meaning that method types may now depend on earlier methods.
  • More flexible class instance resolution, so that function types and lambda expressions can be made instances of a type class.
  • Add !expr notation for implicit binding of intermediate results in monadic/do/etc expressions.
  • Extend Effects package to cope with possibly failing operations, using if_valid, if_error, etc.
  • At the REPL, it now refers to the previous expression.
  • Semantic colouring at the REPL. Turn this off with --nocolour.
  • Some prettifying of error messages.
  • The contents of ~/.idris/repl/init are run at REPL start-up.
  • The REPL stores a command history in ~/.idris/repl/history.
  • The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality checker and can thus be used in types. The [x..] syntax now returns an actually infinite stream.
  • Add %reflection option for functions, for compile-time operations on syntax.
  • Add expression form quoteGoal x by p in e which applies p to the expected expression type and binds the result to x in the scope e.
  • Performance improvements in Strings library.
  • Library reorganisation, separated into prelude and base.

There are several internal changes, mostly improving performance and fixing bugs:

  • New module/dependency tree checking.
  • New parser implementation with more precise errors.
  • Improved type class resolution.
  • Compiling Nat via GMP integers.
  • Performance improvements in elaboration.
  • Improvements in termination checking.
  • Various REPL commands to support interactive editing, and a client/server mode to allow external invocation of REPL commands.

Thanks, as ever, to everyone who has helped put this release together. You can find their names 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.

Idris 0.9.9 released

A new version of Idris, 0.9.9, has been released on hackage. The tutorial has also been updated. The user visible changes are:

  • Apply functions by return type, rather than with arguments:
    • t <== f means "apply f with arguments such that it returns a value of type t"
  • Allow the result type of a rewrite to be specified:
    • rewrite prf ==> ty in val rewrites by prf, and checks that the resulting goal
      type is ty (Example)
  • Allow names to be attached to provisional definitions
    • lhs ?= {name} rhs generates a lemma called 'name' which makes the types of the lhs and rhs match. {name} is optional --- a unique name is generated if it is absent.
  • Experimental LLVM backend
  • Added Data.HVect module
  • Fix fromInteger to take an Integer, rather than an Int.
  • Integer literals for Fin n
  • Renamed O to Z, and fO to fZ to avoid confusion with the digit 0.
  • Swapped Vect arguments, now Vect : Nat -> Type -> Type
  • Added new DecEq instances
  • Add equiv tactic, which rewrites a goal to an equivalent (convertible) goal

Internal changes:

  • Add annotation for unification traces
  • Add mrefine tactic for refining by matching against a type
  • Type class resolution fixes
  • Much faster coverage checking

Thanks to everyone who has helped put this release together.

As always, please report any problems on the github issue tracker. Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.

Idris 0.9.8 released

A new version of Idris, 0.9.8, has been released on hackage. The user visible changes are:

  • Added “rewrite … in …” construct
  • Allow type class constraints in ‘using’ clauses
  • Renamed EFF to EFFECT in Effect package
  • Experimental Java backend
  • Tab completion in REPL
  • Dynamic loading of C libraries in the interpreter
  • Testing IO actions at the REPL
  • Improve rendering of :t
  • Fixed some INTERNAL ERROR messages

Several internal changes have been made:

  • Fix non-linear pattern checking
  • Improved name disambiguation
  • More flexible unification and elaboration of lambdas
  • Various unification and totality checking bug fixes

Thanks to everyone who has helped put this release together.

As always, please report any problems on the github issue tracker. Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.

Idris 0.9.7 released

A new version of Idris, 0.9.7, has been released on hackage. There are only a few user visible changes.

  • implicit keyword, for implicit type conversion
  • Added Effects package, accessed with -p effect
  • Primitives for 8,16,32 and 64 bit integers

There is a small number of internal changes, some of them very large:

  • Changed unification so that it keeps track of failed constraints in case later information helps to resolve them
  • Distinguishing parameters and indices in data types
  • Faster termination/coverage checking
  • Split ‘javascript’ target into ‘javascript’ and ‘node’

Thanks to everyone who has helped put this release together.

As always, please report any problems on the github issue tracker. Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.

Idris 0.9.6 released

A new version of Idris, 0.9.6, has been released on hackage. This release has many updates and improvements. User visible changes are:

  • The type of types is now Type rather than Set
  • Forward declarations of data now allowed
    • supporting induction recursion and mutually recursive data
  • Type inference of definitions in where clauses
    • Provided that the type can be completely determined from the first
      application of the function (in the top level definition)
  • mutual blocks added
    • effect is to elaborate all types of declarations in the block before elaborating their definitions
    • allows inductive-recursive definitions
  • Expression inspected by with clause now abstracted from the goal (i.e. “magic” with)
  • Implicit arguments will be added automatically only if their initial letter is lower case, or they are in a using declaration
  • Added documentation comments (Haddock style) and :doc REPL command
  • Pattern matching on strings, big integers and characters
  • Added System.Concurrency modules
  • Added postulate declarations
  • Allow type annotations on let tactic
  • JavaScript generation, with --target javascript option

Internal changes:

  • Separate inlining methods at compile-time and run-time
  • Fixed nested parameters blocks
  • Improve efficiency of elaborator by:
    • only normalising when necessary
    • reducing backtracking with resolving ambiguities
  • Better compilation of case trees

Thanks to everyone who has helped put this release together.

As always, please report any problems on the github issue tracker. Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.

Idris 0.9.5 released

Idris version 0.9.5 has been released on Hackage. To install, run cabal update and type cabal install idris. This release includes a new termination checker, coinduction, much improved compilation and code generation through more aggressive erasure and inlining, as well as several minor additions and fixes.

It includes the following user visible changes:

  • Added codata declarations
    • as data declarations, but constructor arguments are evaluated lazily
    • functions which return a codata type do not reduce at compile time
  • New termination checker supporting mutually recursive definitions.
  • Added parameters blocks
  • Allow local data definitions in where blocks
  • Added %default directive to declare total-by-default or partial-by-default for functions, and a corresponding partial reserved word to mark functions which are allowed to be partial.
  • Command line options --total and --partial to declare total or partial by default.
  • Command line option --warnpartial for flagging all undeclared partial functions, without error.
  • Added :load command to REPL, for loading a new file
  • Added :module command to REPL, for adding modules
  • Renamed library modules (now have initial capital)

The internal changes are:

  • Added collapsing optimisation and more aggressive erasure
  • Several improvements and fixes to unification

Thanks to everyone who has helped put this release together.

As always, please report any problems on the github issue tracker. Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.