Idris 0.12

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.

Tags c llvm programming-language functional haskell ml agda
License BSDL
State stable

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