Fetching contributors…
Cannot retrieve contributors at this time
206 lines (159 sloc) 6.4 KB
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
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