A new version (0.2.0) of Idris 2 has been released. You can download the source
(including generated Scheme and Racket files for bootstrapping) from the
download page.
The significance of this release is that it is the first release which can
compile itself - that is, it is written in Idris 2. To build it, you can either
use a bootstrapping version built in
Idris 1, or (the simplest way), run make bootstrap to build from the
generated Scheme. Full instructions are in INSTALL.md in the distribution.
Documentation is available here.
To get started, you can see:
The installation has worked successfully on Linux, Windows, Mac and Raspberry
Pi. Please let us know (ideally via the mailing list) how you get on with installing on other
platforms.
The main changes since Idris 2 version 0.1 are:
Language changes
- total, covering and partial flags on functions now have an effect.
- %default <totality status> has been implemented. By default, functions must
be at least covering
- That is, %default covering is the default status.
- Fields of records can be accessed (and updated) using the dot syntax,
such as r.field1.field2 or record { field1.field2 = 42 }.
For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
- New function flag %tcinline which means that the function should be
inlined for the purposes of totality checking (but otherwise not inlined).
This can be used as a hint for totality checking, to make the checker look
inside functions that it otherwise might not.
- To improve error messages, one can use with NS.name <term>
or with [NS.name1, NS.name2, ...] <term> to disable disambiguation
for the given names in <term>. Example: with MyNS.(>>=) do ....
Library additions
- Additional file management operations in base
- New module in base for time (System.Clock)
- New modules in contrib for JSON (Language.JSON.*); random numbers
(System.Random)
Compiler updates
Data types with a single constructor, with a single unerased arguments,
are translated to just that argument, to save repeated packing and unpacking.
(c.f. newtype in Haskell)
- A data type can opt out of this behaviour by specifying noNewtype in its
options list. noNewtype allows code generators to apply special handling
to the generated constructor/deconstructor, for a newtype-like data type,
that would otherwise be optimised away.
0-multiplicity constructor arguments are now properly erased, not just
given a placeholder null value.
Other improvements
- Various performance improvements in the typechecker:
- Noting which metavariables are blocking unification constraints, so that
they only get retried if those metavariables make progress.
- Evaluating fromInteger at compile time.
- Some (not yet documented) features for transforming and optimising:
- %transform directive, for declaring transformation rules on runtime
expressions. Transformation rules are automatically added for top level
implementations of interfaces.
- A %spec flag on functions which allows arguments to be marked for partial
evaluation, following the rules from "Scrapping Your Inefficient Engine"
(ICFP 2010, Brady & Hammond)
- Extend Idris2's literate mode to support reading Markdown and OrgMode files.
For more details see:
https://idris2.readthedocs.io/en/latest/reference/literate.html
Any issues you do find, please report via
the github issue tracker.
We may not be able to fix them quickly (there's not many of us working on
this full time after all) but it's still useful to know what they are!
If you're experimenting with Idris programming, and have a little bit of
experience in Idris 1, we'd encourage you to experiment with Idris 2 now,
as this will be the best way to find and fix any problems. Also, it is
significantly faster :).
Thanks to the many people who have contributed, whether by adding features,
fixing code, reporting issues, or anything else. You can find a list of
contributors
in the GitHub repository.
Have fun!
![[Idris]](https://www.idris-lang.org/images/logo-small.png){kind=logo}