Idris 0.9.4 released

Idris version 0.9.4 has been released on Hackage. To install, run cabal update and type cabal install idris. This is primarily a bug fix release, to correct some teething problems with the new compiler back end.

It includes the following user visible changes:

  • Simple packaging system (see documentation)
  • Added --dumpc flag for displaying generated code

Internal changes:

  • Improve overloading resolution (especially where this is a type error)
  • Various important bug fixes with evaluation and compilation
  • More aggressive compile-time evaluation

As always, please report any problems on the github issue tracker – I will catch up with what is on there eventually! Also, do let me know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.

Idris 0.9.3.1 released

A new version of Idris has been released on hackage. To install, run cabal update and type cabal install idris. To learn more, see the tutorial and FAQ. The user visible changes are:

  • Added binding forms to syntax rules
  • Named class instances
  • Added ‘:set’ command, with options ‘errorcontext’ for displaying local variables in scope when a unification error occurs, and ‘showimplicits’ for displaying elaborated terms in full
  • Added ‘–errorcontext’ command line switch
  • Added ‘:proofs’ and ‘:rmproofs’ commands
  • Various minor REPL improvements and fixes

The internal changes are:

  • Completely new run time system (not based on Epic or relying on Boehm GC)
  • Normalise before forcing to catch more forceable arguments
  • Types no longer exported in normal form
  • Try to resolve overloading by inspecting types, rather than full type checking

Enjoy! Please report any problems on the github issue tracker.

Idris 0.9.2 released

A new version of Idris has been released on hackage. To install, run cabal update and type cabal install idris. To learn more, see the tutorial and FAQ. The tutorial has also been updated.

This version is mostly a bug fix release, with some minor additions to the language. The user visible changes are:

  • backtick notation added: x `foo` y is equivalent to foo x y
  • case expressions now allowed in type signatures
  • Library extensions in prelude.vect, prelude.algebra and prelude.heap
  • malloc and trace_malloc added to builtins, for low level memory management

The internal changes are:

  • Some type class resolution fixes
  • Performance improvements in resolving overloading and type classes
  • Several minor bug fixes

There will no doubt be more bugs. As usual, if you find any, please do not hesitate to contact Edwin Brady (ecb10 at st-andrews dot ac dot uk).

Idris 0.9.1 released

A new version of Idris has been released on hackage. To install, run cabal update and type cabal install idris. To learn more, see the tutorial and FAQ. The tutorial has also been updated.

This version adds some new features, fixes several bugs and has a number of performance improvements. The user visible changes are:

  • DSL notation, for overloading lambda and let bindings
  • Dependent records, with projection and update
  • Totality checking, and total keyword
  • Auto implicit arguments, and default argument values {auto n : T} and {default val n : T}
  • Overlapping type class instances disallowed
  • Many extensions to prelude.nat and prelude.list libraries (mostly thanks to Dominic Mulligan)
  • New libraries: control.monad.identity, control.monad.state
  • Small improvements in error reporting

The internal changes are:

  • Faster compilation (only compiling names which are used)
  • Better type class resolution
  • Lots of minor bug fixes

There will no doubt be bugs. If you find any, please do not hesitate to contact Edwin Brady (ecb10 at st-andrews dot ac dot uk).

Idris 0.9.0 released

A new version of Idris has been released on hackage. To install, run cabal update and type cabal install idris. To learn more, see the tutorial and FAQ.

This version is a complete rewrite. The user visible changes are:

  • New proof/tactics syntax
  • New syntax for pairs/dependent pairs
  • Indentation-significant syntax
  • Added type classes
  • Added where clauses
  • Added case expressions, pattern matching let and lambda
  • Added monad comprehensions
  • Added cumulativity and universe checking
  • Ad-hoc name overloading, resolved by type or explicit namespace
  • Modules (Haskell-style)
  • public, abstract and private access to functions and types
  • Improved interactive environment
  • Replaced ‘do using’ with Monad class
  • Extended syntax macros

The internal changes are:

  • Everything :-). Most importantly, all definitions (functions, classes and instances) are now elaborated to a core language consisting of top level, fully explicit, data declarations and pattern matching definitions, which are verified by a minimal type checker.

This is the first release of a complete reimplementation. There will therefore, no doubt, be bugs. If you find any, please do not hesitate to contact Edwin Brady (ecb10 at st-andrews dot ac dot uk).

New web site

As you might have noticed, I’ve been updating the web site. I have to post something here so that the news feed does something… I will post something more interesting as soon as something more interesting happens.