Idris 0.10 Released

A new version of Idris, 0.10, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. There’s only a small number of changes from version 0.9.20, which are detailed below.

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.

Language Updates

  • The class and instance keywords have been deprecated. The class keyword has been replaced by interface. Instances are now called implementations and are introduced by giving the interface name and parameters. For example:
    interface Eq a where
        (==) : a -> a -> Bool
        (/=) : a -> a -> Bool
    
        (==) x y = not (/=) x y
        (/=) x y = not (==) x y
    
    Eq Bool where
        True  == True  = True
        True  == False = False
        False == True  = False
        False == False = True
    
    Eq a => Eq (Maybe a) where
        Nothing  == Nothing  = True
        Nothing  == (Just _) = False
        (Just _) == Nothing  = False
        (Just a) == (Just b) = a == b
    

    This is as before, but without the instance keyword.

    The rationale for this change is that interfaces as implemented in Idris have several differences from Haskell type classes, even though they have a lot in common. They can be parameterised by things which are not types (including values and interfaces themselves). They are primarily for overloading interfaces, rather than classifying types, and hence there can be multiple implementations.

  • New Fractional interface, with functions (/) and recip.

REPL Updates

  • New command :watch which watches the currently loaded file, and reloads it if it has been changed.

Miscellaneous Updates

  • 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 categories. Default is for all categories to be logged.
  • New flag --listlogcats to list logging categories.

Future Release Plans

Version 1.0 of the Idris language is intended to coincide with the completion of the book
Type Driven Development with Idris. The version of Idris on Hackage will be kept up to date with the latest draft of the book.

Idris is still research software, so 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.20 released

A new version of Idris, 0.9.20, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. Updates are detailed below.

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.

Idris is still research software, so 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.

Language updates

  • Improved unification by implementing a pattern unification rule
  • Changed scoping rules for unbound implicits: any name which would be a valid unbound implicit is now always an unbound implicit. This is much more resilient to changes in inputs, but does require that function names be explicitly qualified when in argument position.
  • Name binding in patterns follows the same rule as name binding for implicits in types: names which begin with lower case letters, not applied to any arguments, are treated as bound pattern variables.
  • The previous syntax for tactic proofs and the previous interactive prover are now deprecated in favour of reflected elaboration. They will be removed at some point in the future.
  • The syntax `{{n}} quotes n without resolving it, allowing short syntax for defining new names. `{n} still quotes n to an existing name in scope.
  • A new primitive operator prim__strSubstr for more efficient extraction of substrings. External code generators should implement this.
  • Added %deprecate directive, which gives a warning and a message when a deprecated name is referenced.

Library updates

  • The Neg class now represents numeric types which can be negative. As such, the (-) operator and abs have been moved there from Num.
  • A special version of (-) on Nat requires that the second argument is smaller than or equal to the first. minus retains the old behaviour, returning Z if there is an underflow.
  • The (+), (-), and (*) operations on Fin have been removed.
  • File IO operations (for example openFile/fread/fwrite) now return Either FileError ty where the return type was previously ty to indicate that they may fail.
  • New Logging Effects have been added to facilitate logging of effectful programmes.
  • Elaborator reflection is now a part of the prelude. It is no longer necessary to import Language.Reflection.Elab.
  • The PERF effect allows for simple performance metrics to be collected from Effectful programs.
  • Some constructors that never actually occurred have been removed from the TT and Raw reflection datatypes in Language.Reflection.

Tool updates

  • Records are now shown as records in :doc, rather than as the underlying datatype
  • iPKG files have a new option pkgs which takes a comma-separated list of package names that the idris project depends on. This reduces bloat in the opts option with multiple package declarations.
  • iPKG files now allow executable = "your filename here" in addition to the existing executable = yourFilenameHere style. While the unquoted version is limited to filenames that look like namespaced Idris identifiers (your.filename.here), the quoted version accepts any valid filename.
  • Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now adds missing clauses if there is already a definition.

Miscellaneous updates

  • Disable the deprecation warnings for %elim and old-style tactic scripts with the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings flags.

Idris 0.9.19 released

A new version of Idris, 0.9.19, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. Updates are detailed below.

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.

Idris is still research software, so 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.

Language changes

  • More flexible case construct, allowing each branch to target different types, provided that the case analysis does not affect the form of any variable used in the right hand side of the case.
  • decl syntax rules to allow syntax extensions at the declaration level
  • As usual, lots of improvements and fixes in elaboration

Library changes

  • The Show class has been moved into Prelude.Show and augmented with the method showPrec, which allows correct parenthesisation of showed terms. This comes with the type Prec of precedences and a few helper functions.
  • Use predicates instead of boolean equality proofs as preconditions on List functions
  • Moved System.Interactive, along with getArgs to the Prelude, in Prelude.Interactive.

Tool changes

  • New REPL command :printerdepth that sets the pretty-printer to only descend to some particular depth when printing. The default is set to a high number to make it less dangerous to experiment with infinite structures. Infinite depth can be set by calling :printerdepth with no argument.
  • Compiler output shows applications of >>= in do-notation
  • fromInteger i where i is an integer constant is now shown just as i in compiler output
  • An interactive shell, similar to the prover, for running reflected elaborator actions. Access it with :elab from the REPL.
  • Major improvements to reflected elaboration scripts, including the ability to run them in a declaration context and many bug fixes.
  • New command-line option --highlight that causes Idris to save highlighting information when successfully type checking. The information is in the same format sent by the IDE mode, and is saved in a file with the extension .idh.
  • Highlighting information is saved by the parser as well, allowing it to highlight keywords like case, of, let, and do
  • Some improvements in interactive editing, particularly in lifting out definitions and proof search. Proof search is now aware of type classes.
  • Experimental Windows support for console colours.

Other changes

Idris 0.9.18 released

A new version of Idris, 0.9.18, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. Updates are detailed below.

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.

Idris is still research software, so 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.

Language changes

  • There is a new syntax for records, corresponding to type class syntax (which is also a record-like structure). See dependent records in the documentation
  • Records can now be coinductive, using the corecord keyword
  • Type class constructors can be given user accessible names (corresponding to the new record syntax)
  • if...then...else is now built in syntax rather than a syntax macro, desugaring to ifThenElse. This is for cleaner overloading and better error messages in domain specific languages.
  • Pattern matching lambdas and case expressions can now be labelled impossible, in
    the same way as top level patterns
  • Added a %hint function annotation, which allows functions to be used in proof search for auto arguments. Only functions which return instances of a data or record type are allowed as hints
  • Strings are now UTF8 encoded, and Idris source is assumed to be UTF8 encoded
  • Some reorganisation of primitives:
    • Buffer and BitVector removed (due to insufficient testing and lack of a maintainer)
    • Float renamed to Double
    • Externally defined primitives now supported with %extern directive
    • Ptr and ManagedPtr removed and replaced with external primitives
  • New quotation syntax `{n} for a quotation of the reflected representation of the name n. If n is lexically bound, then the resulting quotation will be for it, whereas if it is not, then it will succeed with a quotation of the unique global name that matches
  • As usual, lots of improvements and fixes in elaboration, especially with type class resolution
    and name disambiguation

Library changes

  • The default Semigroup and Monoid instances for Maybe are now prioritised choice, keeping the first success as Alternative does. The version that collects successes is now a named instance
  • The return types of Vect.findIndex, Vect.elemIndex and Vect.elemIndexBy were changed from Maybe Nat to Maybe (Fin n)

Tool changes

  • :exec REPL command now takes an optional expression to compile and run/show
  • A new :browse command shows the contents of a namespace
  • Agda-style semantic highlighting is supported over the IDE protocol

Idris 0.9.17 released

A new version of Idris, 0.9.17, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org.

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.

Idris is still research software, so 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.

The main new features and updates are:

  • Library operators have been renamed for consistency with corresponding operators in Haskell. In particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is now an alias for Functor.map. Correspondingly, ($>) and (<$) have been renamed to (<*) and (*>). The cascading effects of this rename are that Algebra.(<*>) has been renamed to Algebra.(<.>) and Matrix.(<.>) is now Matrix.(<:>).
  • Types errors have been improved, now giving the provenance of incorrect types
  • Documentation has been updated and moved to docs.idris-lang.org, hosted by Read the Docs.
  • Web documentation is now available for packages, from the Documentation page.
  • A new package contrib has been added to the libraries. This is for things which are less mature or less used than the contents of base.contrib is not available by default, so you may need to add -p contrib to your .ipkg file or Idris command line.
  • Instances and type providers can now be given documentation strings.
  • Lots of issues relating to type class resolution have been resolved. In particular:
    • Arguments are now checked for injectivity, since this is assumed throughout unification
    • Multi-parameter type classes can now be given determining parameters, which are the parameters used to resolve class instances. Only determining parameters are assumed and checked to be injective.
  • Binding forms in dsl notation are now given an extra argument: a reflected representation of the name that the user chose. Specifically, the rewritten lambda, pi, and let binders will now get an extra argument of type TTName. This allows more understandable dynamic errors in DSL code and more readable code generation results.
  • The Foreign Function Interface has been updated to support multiple back end descriptions.
  • A new FFI_Export type has been added, supporting export of functions to be called by foreign code. Details of the FFI and its interaction with back ends are given in this draft paper.

Idris 0.9.16 released

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

The tutorial has also been updated.

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.

Idris is still research software, so 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.

The main new features and updates are:

  • Inductive-inductive definitions are now supported (i.e. simultaneously defined types where one is indexed by the other)
  • Implicits and type class constraints can now appear in scopes other than the top level
  • Importing a module no longer means it is automatically reexported. A new public modifier has been added to import statements, which will reexport the names exported from that module
  • Implemented @patterns. A pattern of the form x@p on the left hand side matches p, with x in scope on the right hand side with value p
  • Vect, Fin and So moved out of prelude into base, in modules Data.Vect, Data.Fin and Data.So respectively
  • 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
  • :search and :apropos commands can now be given optional package lists to search
  • Better Unicode support for the JavaScript/Node codegen
  • Modules can now have API documentation strings

Additionally, several long-standing issues have been resolved, particularly with pattern matching and coverage checking.

Idris 0.9.15.1 released

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

The tutorial has also been updated.

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.

Idris is still research software, so 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.

The main new features and updates are:

  • Naming of data and type constructors is made consistent across the standard library.
    • Note: This change will break existing code!
    • Data and Type Constructors now consistently begin with a capital letter, which means in particular we have Refl, FZ and FS for refl, fZ and fS.
    • The empty type is now called Void, and its eliminator void.
  • EXPERIMENTAL support for Uniqueness Types
  • EXPERIMENTAL support for Partial Evaluation, as described in Scrapping your Inefficient Engine.
  • The Java and LLVM backends have been factored out into separate projects, idris-java and idris-llvm.

There are several minor updates and improvements:

  • More efficient representation of the proof state, leading to faster elaboration of large expressions.
  • Two new tactics: skip and fail. skip does nothing, and fail takes a string as an argument and produces it as an error, with corresponding reflected tactics.
  • Improved display in the interactive prover.
  • 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.
  • 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.
  • Terms in code blocks in documentation strings are now parsed and type checked. If this succeeds, they are rendered in full colour 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.

Idris 0.9.14 released

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

The tutorial has also been updated.

This release is primarily to improve robustness and efficiency, and solves several long-standing issues. There is also a new, improved, JavaScript backend and better syntactic support for reflection.

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.

Idris is still research software, so 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.

The main new features and updates are:

  • Tactic for case analysis in proofs
  • Induction and case tactic now work on expressions
  • Support for running tests for a package with the tests section of .ipkg files and the --testpkg command-line option
  • Clearly distinguish between type providers and postulate providers at the use site
  • Allow dependent function syntax to be overridden in dsl blocks, similarly to functions and let. The keyword for this is pi.
  • Updated effects library, with simplified API
  • All new JavaScript backend (avoids callstack overflows)
  • Add support for %lib directive for NodeJS
  • Quasiquotes and quasiquote patterns allow easier work with reflected terms.`(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected version of it. Subterms prefixed with ~ are unquoted – on the RHS, they are reflected terms to splice in, while on the LHS they are patterns. A quasiquote expression can be given a goal type for the elaborator, which helps with disambiguation. For instance, `(() : ()) quotes the unit constructor, while `(() : Type) quotes the unit type. Both goal types and quasiquote are typechecked in the global environment.
  • Better inference of unbound implicits.

Idris 0.9.13.1 released

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

This is a bug fix release: it fixes a problem with the interaction between lazy values and the new implementation of erasure introduced in 0.9.13, and slightly improves unification error messages.

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