Idris is a functional programming language with dependent types, where values
are constrained and pattern-matched by an expressive type system to avoid
logic misbehaviours. It's a general purpose language, but also supports
interactive theorem-proving, is sufficient performant trough eager and LLVM
compilation. It has monads, type classes, comprehensions, lambda bindings,
where and with clauses, expressions in case statements, an
indendation-based and extendable syntax, lists, tuples and pairs, and comes
with a Hugs-style REPL.
Homepage
Download
Recent Releases
0.1227 Mar 2016 03:15
minor feature:
:
Improved startup performance by reducing the processing of an already imported.
Module that has changed accessibility.
0.1101 Feb 2016 03:15
minor feature:
:
Updated export rules.
The export rules are:
- 'private' means that the definition is not exported at all.
- 'export' means that the top level type is exported, but not the
definition. In the case of 'data', this means the type constructor is
exported but not the data constructors.
- 'public export' means that the entire definition is exported.
By default, names are 'private'. This can be altered with an access
directive as before.
Exported types can only refer to other exported names.
Publicly exported definitions can only refer to publicly exported names.
Minor language changes.
The ' static ' annotation is changed to ' static' to be consistent with the.
other annotations.
0.10.129 Jan 2016 03:15
minor feature:
:
The ' static ' annotation is changed to ' static' to be consistent with the.
Other annotations.
0.1021 Jan 2016 06:25
minor feature:
:
'class' and 'instance' are now deprecated keywords. They have been.
Replaced by 'interface' and 'implementation' respectively. This is to
Properly reflect their purpose.
(/) operator moved into new Fractional interface.
Idris' logging infrastructure has been categorised. Command line and repl.
Are available. For command line the option `--logging-categories CATS`
is used to pass in the categories. Here `CATS` is a colon separated quoted.
String containing the categories to log. The REPL command is `logcats CATS`.
Where `CATS` is a whitespace separated list of categoriese. Default is for.
All categories to be logged.
New flag `--listlogcats` to list logging categories.`.
0.9.2120 Dec 2015 03:15
minor documentation:
:
Idris' logging infrastructure has been categorised. Command line and repl.
Are available. For command line the option `--logging-categories CATS`
is used to pass in the categories. Here `CATS` is a colon separated quoted.
String containing the categories to log. The REPL command is `logcats CATS`.
Where `CATS` is a whitespace separated list of categoriese. Default is for.
All categories to be logged.
0.9.2002 Sep 2015 07:05
minor documentation:
:
Language updates.
None so far .
Library updates.
None so far .
Tool updates.
None so far .
Miscellaneous updates.
None so far .
0.9.1824 Mar 2015 03:15
minor feature:
:
--------------.
Syntax rules no longer perform variable capture. Users of effects will
need to explicitly name results in dependent effect signatures instead
of using the default name "result".
0.9.1713 Feb 2015 03:25
minor feature:
The --ideslave command line option has been replaced with a --ide-mode
command line option with the same semantics.
0.9.1629 Nov 2014 19:05
minor feature:
A new tactic sourceLocation that fills the current hole with the current
source code span, if this information is available. If not, it raises an
error.
0.9.1528 Oct 2014 18:25
minor feature:
Two new tactics: skip and fail. Skip does nothing, and fail takes a string
as an argument and produces it as an error.
Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list
of ErrorReportParts as an argument, like error handlers produce, allowing
access to the pretty-printer.
Stop showing irrelevant and inaccessible internal names in the interactive
prover.
The proof arguments in the List library functions are now implicit and
solved automatically.
More efficient representation of proof state, leading to faster
elaboration of large expressions.
EXPERIMENTAL Implementation of uniqueness types
Unary negation now desugars to "negate", which is a method of the Neg type
class.
This allows instances of Num that can't be negative, like Nat, and it
makes correct
IEEE Float operations easier to encode. Additionally, unary negation is
now available to DSL authors.
The Java and LLVM backends have been factored out for separate
maintenance. Now, the
compiler distribution only ships with the C and JavaScript backends.
New REPL command :printdef displays the internal definition of a name.
New REPL command :pprint pretty-prints a definition or term with LaTeX or
HTML highlighting.
Naming of data and type constructors is made consistent across the
standard library.
Terms in `code blocks` inside of documentation strings are now parsed and
type checked. If this succeeds, they are rendered in full color in
documentation lookups, and with semantic highlighting for IDEs.
Fenced code blocks in docs defined with the "example" attribute are
rendered as code examples.
Fenced code blocks declared to be Idris code that fail to parse or type
check now provide error messages to IDE clients.
EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
Engine style).