Idris 2 is a purely functional programming language with first class types.
For full installation instructions, see INSTALL.md. Briefly, if
you have Chez Scheme installed, with the executable name
make bootstrap SCHEME=chez
You may need to change
chez to be the local name of your Chez Scheme. This
is often one of
chezscheme9.5 (depending on the
version). On a modern desktop machine, this process (including tests)
should take less than 5 minutes.
Idris 2 is mostly backwards compatible with Idris 1, with some minor exceptions. The most notable user visible differences, which might cause Idris 1 programs to fail to type check, are:
Unbound implicit arguments are always erased, so it is a type error to attempt to pattern match on one.
Simplified resolution of ambiguous names, which might mean you need to explicitly disambiguate more often. As a general rule, Idris 2 will be able to disambiguate between names which have different concrete return types (such as data constructors), or which have different concrete argument types (such as record projections). It may struggle to resolve ambiguities if one name requires an interface to be resolved.
cong function now takes its congruence explicitly as its first argument.
Minor differences in the meaning of export modifiers
public export, which now refer to visibility of names from other
namespaces rather than visibility from other files.
Module names must match the filename in which they are defined (unless the module's name is "Main").
Anything which uses a
%language pragma in Idris 1 is likely to be different.
Notably, elaborator reflection will exist, but most likely in a slightly
different form because the internal details of the elaborator are different.
Prelude is much smaller (and easier to replace with an alternative).
--no-prelude can be used to not implicitly import
let x = val in e no longer computes with
e, instead being
essentially equivalent to
(\x => e) val. This is to make the
let consistent in the presence of
it is hard to push the computation inside the
Instead, you can define functions locally with
let, which do have
computational force, as follows:
let x : ? x = val in e
Watch this space for more details and the rationale for the changes, as I get around to writing it...
Summary of new features:
letbindings are now more expressive, and can be used to define pattern matching functions locally.
caseexpressions, and means fewer annotations are needed in interface declarations.
A significant change in the implementation is that there is an intermediate
TTImp, which is essentially a desugared Idris, and is cleanly
separated from the high level language which means it is potentially usable
as a core language for other high level syntaxes.
The wiki lists the current plugins available for common text editors and their features.