New in 0.9.11: -------------- * Agda-style equational reasoning (in Syntax.PreorderReasoning) * 'case' construct now abstracts over the scrutinee in its type * Added label type 'name (equivalent to the empty type). This is intended for field/effect disambiguation. "name" can be any valid identifier. Two labels are definitionally equal if they have the same name. Internal changes * Faster elaboration * Smaller .ibc files New in 0.9.10: -------------- * Type classes now implemented as dependent records, meaning that method types may now depend on earlier methods. * More flexible class instance resolution, so that function types and lambda expressions can be made instances of a type class. * Add !expr notation for implicit binding of intermediate results in monadic/do/etc expressions. * Extend Effects package to cope with possibly failing operations, using "if_valid", "if_error", etc. * At the REPL, "it" now refers to the previous expression. * Semantic colouring at the REPL. Turn this off with --nocolour. * Some prettifying of error messages. * The contents of ~/.idris/repl/init are run at REPL start-up. * The REPL stores a command history in ~/.idris/repl/history. * The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality checker and can thus be used in types. The [x..] syntax now returns an actually infinite stream. * Add '%reflection' option for functions, for compile-time operations on syntax. * Add expression form 'quoteGoal x by p in e' which applies p to the expected expression type and binds the result to x in the scope e. * Performance improvements in Strings library. * Library reorganisation, separated into prelude/ and base/. Internal changes * New module/dependency tree checking. * New parser implementation with more precise errors. * Improved type class resolution. * Compiling Nat via GMP integers. * Performance improvements in elaboration. * Improvements in termination checking. * Various REPL commands to support interactive editing, and a client/server mode to allow external invocation of REPL commands. New in 0.9.9: ------------- * Apply functions by return type, rather than with arguments: "t <== f" means "apply f with arguments such that it returns a value of type t" * Allow the result type of a rewrite to be specified * Allow names to be attached to provisional definitions lhs ?= {name} rhs -- generates a lemma called 'name' which makes the types of the lhs and rhs match. {name} is optional - a unique name is generated if it is absent. * Experimental LLVM backend * Added Data.HVect module * Fix fromInteger to take an Integer, rather than an Int * Integer literals for Fin * Renamed O to Z, and fO to fZ * Swapped Vect arguments, now Vect : Nat -> Type -> Type * Added DecEq instances * Add 'equiv' tactic, which rewrites a goal to an equivalent (convertible) goal Internal changes * Add annotation for unification traces * Add 'mrefine' tactic for refining by matching against a type * Type class resolution fixes * Much faster coverage checking New in 0.9.8: ------------- User visible changes: * Added "rewrite ... in ..." construct * Allow type class constraints in 'using' clauses * Renamed EFF to EFFECT in Effect package * Experimental Java backend * Tab completion in REPL * Dynamic loading of C libraries in the interpreter * Testing IO actions at the REPL with :x command * Improve rendering of :t * Fixed some INTERNAL ERROR messages Internal changes: * Fix non-linear pattern checking * Improved name disambiguation * More flexible unification and elaboration of lambdas * Various unification and totality checking bug fixes New in 0.9.7: ------------- User visible changes: * 'implicit' keyword, for implicit type conversion * Added Effects package * Primitives for 8,16,32 and 64 bit integers Internal changes: * Change unification so that it keeps track of failed constraints in case later information helps to resolve them * Distinguishing parameters and indices in data types * Faster termination/coverage checking * Split 'javascript' target into 'javascript' and 'node' New in 0.9.6: ------------- User visible changes: * The type of types is now 'Type' rather than 'Set' * Forward declarations of data allowed - supporting induction recursion and mutually recursive data * Type inference of definitions in 'where' clauses - Provided that the type can be completely determined from the first application of the function (in the top level definition) * 'mutual' blocks added - effect is to elaborate all types of declarations in the block before elaborating their definitions - allows inductive-recursive definitions * Expression inspected by 'with' clause now abstracted from the goal - i.e. "magic" with * Implicit arguments will be added automatically only if their initial letter is lower case, or they are in a using declaration * Added documentation comments (Haddock style) and ':doc' REPL command * Pattern matching on strings, big integers and characters * Added System.Concurrency modules * Added 'postulate' declarations * Allow type annotations on 'let' tactic * EXPERIMENTAL JavaScript generation, with '--target javascript' option Internal changes: * Separate inlining methods at compile-time and run-time * Fixed nested parameters blocks * Improve efficiency of elaborator by: - only normalising when necessary - reducing backtracking with resolving ambiguities * Better compilation of case trees New in 0.9.5: ------------- User visible changes: * Added codata - as data declarations, but constructor arguments are evaluated lazily - functions which return a codata type do not reduce at compile time * Added 'parameters' blocks * Allow local data definitions in where blocks * Added '%default' directive to declare total-by-default or partial-by-default for functions, and a corresponding "partial" reserved words to mark functions as allowed to be partial. Also "--total" and "--partial" added as command line options. * Command line option "--warnpartial" for flagging all undeclared partial functions, without error. * New termination checker supporting mutually recursive definitions. * Added ':load' command to REPL, for loading a new file * Added ':module' command to REPL, for adding modules * Renamed library modules (now have initial capital) Internal changes: * Several improvements and fixes to unification * Added collapsing optimisation and more aggressive erasure New in 0.9.4: ------------- User visible changes: * Simple packaging system * 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 New in 0.9.3: ------------- User visible changes: * 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 Internal changes: * 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 New in 0.9.2: ------------- User visible changes: * backtick notation added: x `foo` y ==> foo x y * case expressions allowed in type signatures * Library extensions in prelude.vect and prelude.algebra * malloc/trace_malloc added to builtins.idr Internal changes: * Some type class resolution fixes * Several minor bug fixes * Performance improvements in resolving overloading and type classes New in 0.9.1: ------------- User visible changes: * DSL notation, for overloading lambda and let bindings * Dependent records, with projection and update * Totality checking and 'total' keyword * Auto implicits and default argument values {auto n : T}, {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 Internal changes: * Faster compilation (only compiling names which are used) * Better type class resolution * Lots of minor bug fixes 0.1.x to 0.9.0: Complete rewrite. User visible changes: * 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 * Separate type-checking * Improved interactive environment * Replaced 'do using' with Monad class * Extended syntax macros Internal changes: * Everything :-) * All definitions (functions, classes and instances) are elaborated to 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 be bugs. If you find any, please do not hesitate to contact Edwin Brady (ecb10@st-andrews.ac.uk).