3* The Idris Reference manual has been fleshed out with content originally found
5* The Show class has been moved into Prelude.Show and augmented with the method
6 showPrec, which allows correct parenthesization of showed terms. This comes
7 with the type Prec of precedences and a few helper functions.
8* New REPL command :printerdepth that sets the pretty-printer to only descend to
9 some particular depth when printing. The default is set to a high number to
10 make it less dangerous to experiment with infinite structures. Infinite depth
11 can be set by calling :printerdepth with no argument.
12* Compiler output shows applications of >>= in do-notation
13* fromInteger i where i is an integer constant is now shown just as i in
15* An interactive shell, similar to the prover, for running reflected elaborator
16 actions. Access it with :elab from the REPL.
17* New command-line option --highlight that causes Idris to save highlighting
18 information when successfully type checking. The information is in the same
19 format sent by the IDE mode, and is saved in a file with the extension ".idh".
20* Highlighting information is saved by the parser as well, allowing it to highlight
21 keywords like "case", "of", "let", and "do"
22* Use predicates instead of boolean equality proofs as preconditions
24* More flexible 'case' construct, allowing each branch to target different
25 types, provided that the case analysis does not affect the form of any
26 variable used in the right hand side of the case.
27* Some improvements in interactive editing, particularly in lifting out
28 definitions and proof search.
29* Moved System.Interactive, along with getArgs to the Prelude.
33* GHC 7.10 compatibility
34* Add support for bundled toolchains.
35* Strings are now UTF8 encoded in the default back end
36* Idris source files are now assumed to be in UTF8, regardless of locale
38* Some reorganisation of primitives:
39 + Buffer and BitVector primitives have been removed (they were not
40 tested sufficiently, and lack a maintainer)
41 + Float has been renamed 'Double' (Float is defined in the Prelude for
43 + Externally defined primitives and operations now supported with
44 '%extern' directive, allowing back ends to define their own special
46 + Ptr and ManagedPtr have been removed and replaced with external primitives
47* Add %hint function annotation, which allows functions to be used as
48 hints in proof search for 'auto' arguments. Only functions which return
49 an instance of a data or record type are allowed as hints.
50* Syntax rules no longer perform variable capture. Users of effects will
51 need to explicitly name results in dependent effect signatures instead
52 of using the default name "result".
53* Pattern-matching lambdas are allowed to be impossible. For example,
54 Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of
55 requiring a separate lemma.
56* Case alternatives are allowed to be impossible:
57 case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
58* The default Semigroup and Monoid instances for Maybe are now prioritised
59 choice, keeping the first success as Alternative does. The version that
60 collects successes is now a named instance.
61* :exec REPL command now takes an optional expression to compile and run/show
62* The return types of `Vect.findIndex`, `Vect.elemIndex` and
63 `Vect.elemIndexBy` were changed from `Maybe Nat` to `Maybe (Fin n)`
64* A new :browse command shows the contents of a namespace
65* `{n} is syntax for a quotation of the reflected representation of the name
66 "n". If "n" is lexically bound, then the resulting quotation will be for it,
67 whereas if it is not, then it will succeed with a quotation of the unique
68 global name that matches.
69* New syntax for records that closely matches our other record-like structures:
70 type classes. See the updated tutorial for details.
71* Records can be coinductive. Define coinductive records with the "corecord"
73* Type class constructors can be assigned user-accessible names. This is done
74 using the same syntax as record constructors.
75* if ... then ... else ... is now built-in syntax instead of being defined in
76 a library. It is shown in REPL output and error messages, rather than its
78* The desugaring of if ... then ... else ... has been renamed to ifThenElse from
79 boolElim. This is for consistency with GHC Haskell and scala-virtualized, and
80 to reflect that if-notation makes sense with non-Bool datatypes.
81* Agda-style semantic highlighting is supported over the IDE protocol.
82* Experimental support for elaborator reflection. Users can now script the
83 elaborator, for use in code generation and proof automation. This feature is
84 still under rapid development and is subject to change without notice. See
85 Language.Reflection.Elab and the %runElab constructs
90* The --ideslave command line option has been replaced with a --ide-mode
91 command line option with the same semantics.
92* A new tactic "claim N TY" that introduces a new hole named N with type TY
93* A new tactic "unfocus" that moves the current hole to the bottom of the
95* Quasiquotation supports the generation of Language.Reflection.Raw terms
96 in addition to Language.Reflection.TT. Types are used for disambiguation,
97 defaulting to TT at the REPL.
98* Language.Reflection.Quotable now takes an extra type parameter which
99 determines the type to be quoted to. Instances are provided to quote
100 common types to both TT and Raw.
101* Library operators have been renamed for consistency with Haskell. In
102 particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is
103 now an alias for Functor.map. Correspondingly, ($>) and (<$) have
104 been renamed to (<*) and (*>). The cascading effects of this rename
105 are that Algebra.(<*>) has been renamed to Algebra.(<.>) and
106 Matrix.(<.>) is now Matrix.(<:>).
107* Binding forms in DSL notation are now given an extra argument: a
108 reflected representation of the name that the user chose.
109 Specifically, the rewritten lambda, pi, and let binders will now get
110 an extra argument of type TTName. This allows more understandable
111 dynamic errors in DSL code and more readable code generation results.
112* DSL notation can now be applied with $
113* Added FFI_Export type which allows Idris functions to be exportoed and
114 called from foreign code
115* Instances can now have documentation strings.
116* Type providers can have documentation strings.
117* Unification errors now (where possible) contain information about provenance
119* New REPL command ":core TM" that shows the elaborated form of TM along with
120 its elaborated type using the syntax of TT. IDE mode has a corresponding
121 command :elaborate-term for serialized terms.
122* Effectful and IO function names for sending data to STDOUT have been
123 aligned, semantically.
124 + `print` is now for putting showable things to STDOUT.
125 + `printLn` is for putting showable things to STDOUT with a new line
126 + `putCharLn` for putting a single character to STDOUT, with a new line.
127* Classes can now be annotated with 'determining parameters' to say which
128 must be available before resolving instances. Only determining parameters
129 are checked when checking for overlapping instances.
130* New package 'contrib' containing things that are less mature or less used
131 than the contents of 'base'. 'contrib' is not available by default, so you
132 may need to add '-p contrib' to your .ipkg file or Idris command line.
133* Arguments to class instances are now checked for injectivity.
134 Unification assumes this, so we need to check when instances are defined.
138* Inductive-inductive definitions are now supported (i.e. simultaneously
139 defined types where one is indexed by the other.)
140* Implicits and type class constraints can now appear in scopes other than
142* Importing a module no longer means it is automatically reexported. A new
143 "public" modifier has been added to import statements, which will reexport
144 the names exported from that module.
145* Implemented @-patterns. A pattern of the form x@p on the left hand side
146 matches p, with x in scope on the right hand side with value p.
147* A new tactic sourceLocation that fills the current hole with the current
148 source code span, if this information is available. If not, it raises an
150* Better Unicode support for the JavaScript/Node codegen
151* ':search' and ':apropos' commands can now be given optional package lists
153* Vect, Fin and So moved out of prelude into base, in modules Data.Vect,
154 Data.Fin and Data.So respectively.
155* Several long-standing issues resolved, particularly with pattern matching
156 and coverage checking.
157* Modules can now have API documentation strings.
161* Two new tactics: skip and fail. Skip does nothing, and fail takes a string
162 as an argument and produces it as an error.
163* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list
164 of ErrorReportParts as an argument, like error handlers produce, allowing
165 access to the pretty-printer.
166* Stop showing irrelevant and inaccessible internal names in the interactive
168* The proof arguments in the List library functions are now implicit and
169 solved automatically.
170* More efficient representation of proof state, leading to faster elaboration
171 of large expressions.
172* EXPERIMENTAL Implementation of uniqueness types
173* Unary negation now desugars to "negate", which is a method of the Neg type class.
174 This allows instances of Num that can't be negative, like Nat, and it makes correct
175 IEEE Float operations easier to encode. Additionally, unary negation is now available
177* The Java and LLVM backends have been factored out for separate maintenance. Now, the
178 compiler distribution only ships with the C and JavaScript backends.
179* New REPL command :printdef displays the internal definition of a name
180* New REPL command :pprint pretty-prints a definition or term with LaTeX or
182* Naming of data and type constructors is made consistent across the standard
184* Terms in `code blocks` inside of documentation strings are now parsed and
185 type checked. If this succeeds, they are rendered in full color in
186 documentation lookups, and with semantic highlighting for IDEs.
187* Fenced code blocks in docs defined with the "example" attribute are rendered
189* Fenced code blocks declared to be Idris code that fail to parse or type check now
190 provide error messages to IDE clients.
191* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
196* Tactic for case analysis in proofs
197* Induction and case tactic now work on expressions
198* Support for running tests for a package with the tests section of .ipkg files and the
199 --testpkg command-line option
200* Clearly distinguish between type providers and postulate providers at the use site
201* Allow dependent function syntax to be overridden in dsl blocks, similarly to
202 functions and let. The keyword for this is "pi".
203* Updated 'effects' library, with simplified API
204* All new JavaScript backend (avoids callstack overflows)
205* Add support for %lib directive for NodeJS
206* Quasiquotes and quasiquote patterns allow easier work with reflected terms.
207 `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected
208 version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected
209 terms to splice in, while on the LHS they are patterns.
210 A quasiquote expression can be given a goal type for the elaborator, which helps with
211 disambiguation. For instance, `(() : ()) quotes the unit constructor, while `(() : Type)
212 quotes the unit type.
213 Both goal types and quasiquote are typechecked in the global environment.
214* Better inference of unbound implicits
218* IDE support for retrieving structured information about metavariables
219* Experimental Bits support for JavaScript
220* IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
221* Command line option -e (or --eval) to evaluate expressions without loading the
222 REPL. This is useful for writing more portable tests.
223* Many more of the basic functions and datatypes are documented.
224* Primitive types such as Int and String are documented
225* Removed javascript lib in favor of idris-hackers/iQuery
226* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)
227* Remove :info REPL command, subsume and enhance its functionality in the :doc command
228* New (first class) nested record update/access syntax:
229 record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val
230 record { a->b->c } x -- accesses field, equivalent to c (b (a x))
231* The banner at startup can be suppressed by adding :set nobanner to the initialisation script.
232* :apropos now accepts space-delimited lists of query items, and searches for the conjunction
233 of its inputs. It also accepts binder syntax as search strings - for instance, -> finds
235* Totality errors are now treated as warnings until code generation time, when they become
236 errors again. This allows users to use the interactive editing features to fix totality
237 issues, but no programs that violate the stated assumptions will actually run.
238* Added :makelemma command, which adds a new top level definition to solve
240* Extend :addclause to add instance bodies as well as definitions
241* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
242* Move foldl into Foldable so it can be overridden.
243* Experimental :search REPL command for finding functions by type
247* New implementation of erasure
252* Proof search now works for metavariables in types, giving some interactive
254* New 'Lazy' type, replacing laziness annotations.
255* JavaScript and Node codegen now understand the %include directive.
256* Concept of 'null' is now understood in the JavaScript and Node codegen.
257* Lots of performance patches for generated JavaScript.
258* New commands :eval (:e) and :type (:t) in the prover, which either normalise
259 or show the type of expressions.
260* Allow type providers to return postulates in addition to terms.
261* Syntax for dealing with match failure in <- and pattern matching let.
262* New syntax for inline documentation. Documentation starts with |||, and
263 arguments are documented by preceding their name with @. Example:
264 ||| Add two natural numbers
265 ||| @ n the first number (examined by the function)
266 ||| @ m the second number (not examined)
267 plus (n, m : Nat) -> Nat
268* Allow the auto-solve behaviour in the prover to be disabled, for easier
269 debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
270* Updated 'effects' library
271* New :apropos command at REPL to search documentation, names, and types
272* Unification errors are now slightly more informative
273* Support mixed induction/coinduction with 'Inf' type
274* Add 'covering' function option, which checks whether a function and all
275 descendants cover all possible inputs
280* Agda-style equational reasoning (in Syntax.PreorderReasoning)
281* 'case' construct now abstracts over the scrutinee in its type
282* Added label type 'name (equivalent to the empty type).
283 This is intended for field/effect disambiguation. "name" can be any
284 valid identifier. Two labels are definitionally equal if they have the
286* General improvements in error messages, especially %error_reverse
287 annotation, which allows a hint as to how to display a term in error
289* --ideslave mode now transmits semantic information about many of the
290 strings that it emits, which can be used by clients to implement
291 semantic highlighting like that of the REPL. This has been implemented
292 in the Emacs mode and the IRC bot, which can serve as examples.
293* New expression form: with NAME EXPR privileges the namespace NAME
294 when disambiguating overloaded names. For example, it is possible to
295 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
296 because the Vect constructors are defined in a namespace called Vect.
297* assert_smaller internal function, which marks an expression as smaller than
298 a pattern for use in totality checking.
299 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
300 structurally smaller than "(x :: xs)"
301* assert_total internal function, which marks a subexpression as assumed to
302 be total, e.g "assert_total (tail (x :: xs))".
303* Terminal width is automatically detected if Idris is compiled with curses
304 support. If curses is not available, automatic mode assumes 80 columns.
305* Changed argument order for Prelude.Either.either.
306* Experimental 'neweffects' library, intended to replace 'effects' in the
313* Pretty-printer now used for all term output
319* Type classes now implemented as dependent records, meaning that method
320 types may now depend on earlier methods.
321* More flexible class instance resolution, so that function types and lambda
322 expressions can be made instances of a type class.
323* Add !expr notation for implicit binding of intermediate results in
324 monadic/do/etc expressions.
325* Extend Effects package to cope with possibly failing operations, using
326 "if_valid", "if_error", etc.
327* At the REPL, "it" now refers to the previous expression.
328* Semantic colouring at the REPL. Turn this off with --nocolour.
329* Some prettifying of error messages.
330* The contents of ~/.idris/repl/init are run at REPL start-up.
331* The REPL stores a command history in ~/.idris/repl/history.
332* The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality
333 checker and can thus be used in types. The [x..] syntax now returns an
334 actually infinite stream.
335* Add '%reflection' option for functions, for compile-time operations on
337* Add expression form 'quoteGoal x by p in e' which applies p to the expected
338 expression type and binds the result to x in the scope e.
339* Performance improvements in Strings library.
340* Library reorganisation, separated into prelude/ and base/.
344* New module/dependency tree checking.
345* New parser implementation with more precise errors.
346* Improved type class resolution.
347* Compiling Nat via GMP integers.
348* Performance improvements in elaboration.
349* Improvements in termination checking.
350* Various REPL commands to support interactive editing, and a client/server
351 mode to allow external invocation of REPL commands.
356* Apply functions by return type, rather than with arguments:
357 "t <== f" means "apply f with arguments such that it returns a value
359* Allow the result type of a rewrite to be specified
360* Allow names to be attached to provisional definitions
361 lhs ?= {name} rhs -- generates a lemma called 'name' which makes the
362 types of the lhs and rhs match. {name} is optional - a unique name is
363 generated if it is absent.
364* Experimental LLVM backend
365* Added Data.HVect module
366* Fix fromInteger to take an Integer, rather than an Int
367* Integer literals for Fin
368* Renamed O to Z, and fO to fZ
369* Swapped Vect arguments, now Vect : Nat -> Type -> Type
370* Added DecEq instances
371* Add 'equiv' tactic, which rewrites a goal to an equivalent (convertible) goal
375* Add annotation for unification traces
376* Add 'mrefine' tactic for refining by matching against a type
377* Type class resolution fixes
378* Much faster coverage checking
385* Added "rewrite ... in ..." construct
386* Allow type class constraints in 'using' clauses
387* Renamed EFF to EFFECT in Effect package
388* Experimental Java backend
389* Tab completion in REPL
390* Dynamic loading of C libraries in the interpreter
391* Testing IO actions at the REPL with :x command
392* Improve rendering of :t
393* Fixed some INTERNAL ERROR messages
397* Fix non-linear pattern checking
398* Improved name disambiguation
399* More flexible unification and elaboration of lambdas
400* Various unification and totality checking bug fixes
407* 'implicit' keyword, for implicit type conversion
408* Added Effects package
409* Primitives for 8,16,32 and 64 bit integers
413* Change unification so that it keeps track of failed constraints in case
414 later information helps to resolve them
415* Distinguishing parameters and indices in data types
416* Faster termination/coverage checking
417* Split 'javascript' target into 'javascript' and 'node'
424* The type of types is now 'Type' rather than 'Set'
425* Forward declarations of data allowed
426 - supporting induction recursion and mutually recursive data
427* Type inference of definitions in 'where' clauses
428 - Provided that the type can be completely determined from the first
429 application of the function (in the top level definition)
430* 'mutual' blocks added
431 - effect is to elaborate all types of declarations in the block before
432 elaborating their definitions
433 - allows inductive-recursive definitions
434* Expression inspected by 'with' clause now abstracted from the goal
436* Implicit arguments will be added automatically only if their initial
437 letter is lower case, or they are in a using declaration
438* Added documentation comments (Haddock style) and ':doc' REPL command
439* Pattern matching on strings, big integers and characters
440* Added System.Concurrency modules
441* Added 'postulate' declarations
442* Allow type annotations on 'let' tactic
443* EXPERIMENTAL JavaScript generation, with '--target javascript' option
447* Separate inlining methods at compile-time and run-time
448* Fixed nested parameters blocks
449* Improve efficiency of elaborator by:
450 - only normalising when necessary
451 - reducing backtracking with resolving ambiguities
452* Better compilation of case trees
460 - as data declarations, but constructor arguments are evaluated lazily
461 - functions which return a codata type do not reduce at compile time
462* Added 'parameters' blocks
463* Allow local data definitions in where blocks
464* Added '%default' directive to declare total-by-default or partial-by-default
465 for functions, and a corresponding "partial" reserved words to mark functions
466 as allowed to be partial. Also "--total" and "--partial" added as command
468* Command line option "--warnpartial" for flagging all undeclared
469 partial functions, without error.
470* New termination checker supporting mutually recursive definitions.
471* Added ':load' command to REPL, for loading a new file
472* Added ':module' command to REPL, for adding modules
473* Renamed library modules (now have initial capital)
477* Several improvements and fixes to unification
478* Added collapsing optimisation and more aggressive erasure
485* Simple packaging system
486* Added --dumpc flag for displaying generated code
490* Improve overloading resolution (especially where this is a type error)
491* Various important bug fixes with evaluation and compilation
492* More aggressive compile-time evaluation
499* Added binding forms to syntax rules
500* Named class instances
501* Added ':set' command, with options 'errorcontext' for displaying local
502 variables in scope when a unification error occurs, and 'showimplicits'
503 for displaying elaborated terms in full
504* Added '--errorcontext' command line switch
505* Added ':proofs' and ':rmproofs' commands
506* Various minor REPL improvements and fixes
510* Completely new run time system (not based on Epic or relying on Boehm GC)
511* Normalise before forcing to catch more forceable arguments
512* Types no longer exported in normal form
513* Try to resolve overloading by inspecting types, rather than full type
521* backtick notation added: x `foo` y ==> foo x y
522* case expressions allowed in type signatures
523* Library extensions in prelude.vect and prelude.algebra
524* malloc/trace_malloc added to builtins.idr
528* Some type class resolution fixes
529* Several minor bug fixes
530* Performance improvements in resolving overloading and type classes
537* DSL notation, for overloading lambda and let bindings
538* Dependent records, with projection and update
539* Totality checking and 'total' keyword
540* Auto implicits and default argument values {auto n : T}, {default val n : T}
541* Overlapping type class instances disallowed
542* Many extensions to prelude.nat and prelude.list libraries (mostly thanks to
544* New libraries: control.monad.identity, control.monad.state
545* Small improvements in error reporting
549* Faster compilation (only compiling names which are used)
550* Better type class resolution
551* Lots of minor bug fixes
555Complete rewrite. User visible changes:
557* New proof/tactics syntax
558* New syntax for pairs/dependent pairs
559* Indentation-significant syntax
562* Added case expressions, pattern matching let and lambda
563* Added monad comprehensions
564* Added cumulativity and universe checking
565* Ad-hoc name overloading
566 - Resolved by type or explicit namespace
567* Modules (Haskell-style)
568* public, abstract and private access to functions and types
569* Separate type-checking
570* Improved interactive environment
571* Replaced 'do using' with Monad class
572* Extended syntax macros
577* All definitions (functions, classes and instances) are elaborated to top
578 level, fully explicit, data declarations and pattern matching definitions,
579 which are verified by a minimal type checker.
581This is the first release of a complete reimplementation. There will be bugs.
582If you find any, please do not hesitate to contact Edwin Brady
583(ecb10@st-andrews.ac.uk).
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list