1# New since last release
2+ Updated to work with GHC 8.8 and cabal 3.0
5+ Documentation added to proof section
8+ `openFile` opens the file in binary mode on Windows.
9+ Added library functions `clockTime` and `fRemove`
12+ Modules no longer require building if imports have changed but all
13 interfaces (i.e. types for names declared `export` and definitions of names
14 declared `public export`) are unchanged.
15+ The result of calling `:doc` now details the accessbility of items as well as their totality.
17## Miscellaneous updates
18+ Compiler flag `--optimise-nat-like-types` enables compilation
19 of `Nat`-like type families to big integers. A type family
20 is `Nat`-like if, after erasure, it has two constructors,
21 one nullary, the other one with exactly one recursive field.
26+ Fixes for building with GHC 8.6
27+ Fix for megaparsec update
28+ Some fixes for memory allocation issues in the C back end
33+ Old 'induction' tactics and eliminator generation functionality ('%elim', '%case', 'elim_for') is no longer supported.
34 Please, rely on the ones provided by Pruviloj and elaborator reflection instead.
38+ Changed rndInt in Effect.Random so that it does not alternate between odd
40+ Additions to `contrib`:
41 * `Data.SortedBag`: Bag (or Multiset) implemention based on `Data.SortedMap`.
42 * `Data.PosNat`: A `Nat` paired with a proof that it is positive.
43 * `Data.Chain`: A function with an arbitrary number of arguments, plus
44 combinators for working with them.
47+ Added a switch `--allow-capitalized-pattern-variables` to optionally allow capitalized pattern variables after they were prohibited in 1.2.0.
48+ REPL now prints an error message if program compiled by `:exec` terminates
50+ Idris now builds with GHC 8.4.
51+ In the C backend, the representation of Idris values at runtime has been reworked.
57+ In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side
58 of any definitions in `where` clauses, provided the left-hand side of the
59 definition does not shadow it.
60+ The `LinearTypes` language extension has been revised. It implements the
61 rules from Bob Atkey's draft "The Syntax and Semantics of Quantitative
62 Type Theory" and now works with holes and case expressions.
63+ Backticked operators can appear in sections, e.g. ``(`LTE` 42)`` or
65+ Backticked operators can have their precendence and associativity set like
66 other operators, e.g. ``infixr 8 `cons` ``. Backticked operators with
67 undeclared fixity are treated as non-associative with precedence lower
68 than all declared operators.
69+ Allow non-injective implementations if explicitly named, e.g.,
72 LTB b = DPair Nat (\ n => LT n b)
74 implementation [uninhabltb] Uninhabited (LTB Z) where
75 uninhabited (MkDPair n prf) = absurd prf
77 It is possible to use `using implementation uninhabltb` to add the
78 implementation to the automated resolution, but if it fails to find the
79 instance due to non-injectivity, one must pass it explicitly to target
80 function, i.e. `absurd @{uninhabltb}`.
81+ Verbatim strings now support trailing quote characters. All quote characters
82 until the final three are considered part of the string. Now a string such as
83 `""""hello""""` will parse, and is equivalent to `"\"hello\""`.
84+ C FFI now supports pasting in any expression by prefixing it with '#', e.g.
87 intMax = foreign FFI_C "#INT_MAX" (IO Int)
89+ The deprecated keywords `%assert_total`, `abstract`, and `[static]` have
90 been removed as well as the use of "public" instead of "public export" to
92+ The syntax for pattern-match alternatives now works for `let` statements in
93 `do` blocks in addition to `let` expressions and `<-` statements, e.g.
96 let Just x = expr | Nothing => empty
99 This means that a `with`-application (using `|`) cannot be used in that
104+ Removed `oldeffects` library from `libs` folder, use `effects` or `Control.ST` instead.
105+ Added `Text.Literate`, a module for working with literate source files.
106+ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.
107+ Added `discriminate` and `construct` tactics to Pruviloj.
108+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
109+ Added `Data.IOArray`, containing primitives for mutable arrays.
110+ Added `Language.JSON`, for total serialization/deserialization of JSON data.
111+ Reworked operator fixity for many operators.
112 * Changed `&&` and `||` to be right-associative. Increased precedence of `&&`
113 to be higher than that of `||`.
114 * Removed associativity from Boolean comparison operators `==`, `/=`, `<`, `<=`,
115 `>`, and `>=`. Increased precedence of `/=` and `==` to match the others.
116 * Made `<|>`, `<$>`, and `.` right-associative.
117 * Swapped precedence of `<|>` and `<*>` (and its related operators, `<*` and
118 `*>`). Now `<|>` has a lower precedence.
119 * Lowered the precedence of `>>=` to be below that of `<|>`.
120+ Added some useful string manipulation functions to `Data.String.Extra`.
121+ Added `Control.Delayed`, a module for conditionally making a type `Inf` or `Lazy`.
122+ Added `Data.Fuel`, which implements the `Fuel` data type and the partial `forever` function.
123+ Added `Data.Bool.Extra`, a module with properties of boolean operations.
124+ Moved core of `Text.Lexer` to `Text.Lexer.Core`. Added several new combinators
125 and lexers to `Text.Lexer`.
126+ Moved core of `Text.Parser` to `Text.Parser.Core`. Added several new combinators
127 to `Text.Parser`. Made the following changes.
128 * Flipped argument order of `parse`.
129 * Renamed `optional` to `option` and flip argument order.
130 * Renamed `maybe` to `optional`.
131 * Generalised many combinators to use an unknown `commit` flag where possible.
132+ `Prelude.Doubles.atan2` is now implemented as a primitive instead of
133 being coded in Idris.
134+ Added `Test.Unit` to `contrib` for simple unit testing.
135+ Removed several deprecated items from the libraries shipped with Idris.
136+ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`
137 implements `Abs` with `abs = id`.
138+ Added `Control.ST.File`, an ST based implementation of the same behaviour
139 implemented by `Effect.File` in the effects package.
143+ Private functions are no longer visible in the REPL except for modules
144 that are explicitly loaded.
145+ The --interface option now creates CommonJS modules on the node backend.
146+ The C backend now pass arguments to the C compiler in the same order
147 as they were given in the source files.
148+ Backslash, braces and percent symbols are now correctly pretty printed
150+ Errors and warnings now consistently have the following format:
154 1 | data nat : Type where --error
156 Main.nat has a name which may be implicitly bound.
157 This is likely to lead to problems!
159 The code is highlighted when highlighting information is available. How
160 much highlighting information is available depends on where the error
162+ The parser provider has been switched from Trifecta to Megaparsec. This
163 could possibly cause some subtle deviations in parsing from previous
165+ Many more errors now report beginning *and* ending position (which may be
166 on different lines), instead of just a single point. The format is
167 `Foo.idr:9:7-15:` if ending column is on the same line or
168 `Foo.idr:9:7-10:15:` if the ending column is on a different line.
169+ Error messages were changed so that the last column is inclusive, e.g.
170 `Foo.idr:9:7-15:` includes column 15. Previously the error would have read
175+ Package names now only accept a restrictive charset of letters, numbers and the `-_` characters.
176 Package names are also case insensitive.
177+ When building makefiles for the FFI, the environment variables
178 `IDRIS_INCLUDES` and `IDRIS_LDFLAGS` are now set with the correct C
183+ Erasure analysis is now faster thanks to a bit smarter constraint solving.
184+ Fixed installation issue
185+ Fixed a potential segfault when concatenating strings
191+ Added `Text.PrettyPrint.WL` an implementation of the Wadler-Leijen
192 Pretty-Print algorithm. Useful for those wishing to pretty print
194+ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries
195 for implementing total lexical analysers and parsers.
197 + Added `Catchable` for `ReaderT`, `WriterT`, and `RWST`.
198 + Added `MonadTrans` for `RWST`.
199+ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
200 most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
201+ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
202 mapping from `a` to `Nat`. For example, there is an implementation for lists,
203 where `size = length`.
205 The function `sizeAccessible` then proves well-foundedness of the relation
206 `Smaller x y = LT (size x) (size y)`, which allows us to use strong
207 induction conveniently with any type that implements `Sized`.
209 In practice, this allows us to write functions that recurse not only on
210 direct subterms of their arguments but on any value
211 with a (strictly) smaller `size`.
213 A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
214+ Added utility lemma `decEqSelfIsYes : decEq x x = Yes Refl` to
215 `Decidable.Equality`. This is primarily useful for proving properties of
216 functions defined with the help of `decEq`.
220+ New JavaScript code generator that uses an higher level intermediate
223+ Various optimizations of the new JavaScript code generator.
225+ Names are now annotated with their representations over the IDE
226 protocol, which allows IDEs to provide commands that work on special
227 names that don't have syntax, such as case block names.
238+ Added `Data.Buffer` to `base`. This allows basic manipulation of mutable
239 buffers of `Bits8`, including reading from and writing to files.
243+ Idris now checks the list of packages specified at the command line
244 against those installed. If there is a mismatch Idris will complain.
246## Miscellaneous Updates
248+ Documentation updates for the new `Control.ST` library
249+ Various stability/efficiency fixes
255* Language pragmas now required for the less stable existing features, in
256 addition to the existing `TypeProviders` and `ErrorReflection`:
257 + `ElabReflection`, which must be enabled to use `%runElab`
258 + `UniquenessTypes`, which must be enabled to use `UniqueType`
259 + `DSLNotation`, which must be enabled to define a `dsl` block
260 + `FirstClassReflection`, which must be enabled to define a `%reflection`
263* New language extension `LinearTypes`:
264 + This allows adding a /multiplicity/ to a binder which says how often it
265 is allowed to be used; either 0 or 1 (if unstated, multiplicity is "many")
266 + The typing rules follow Conor McBride's paper "I Got Plenty o' Nuttin'"
267 + This is highly experimental, unfinished, not at all polished. and there
268 are still lots of details to sort out. Some features don't quite work
269 properly yet. But it is there to play with for the brave!
273+ Idris' output has been updated to more accurately reflect its
274 progress through the compiler i.e. Type Checking; Totality Checking;
275 IBC Generation; Compiling; and Code Generation. To control the
276 loudness of the reporting three verbosity levels are introduced:
277 `--V0`, `--V1`, and `--V2`. The old aliases of `-V` and `--verbose`
280+ New REPL command `:!` that runs an external shell command.
282+ The REPL now colourises output on MinTTY consoles (e.g., Cygwin and MSYS)
283 on Windows, which previously did not occur due to a bug.
285+ Idris now runs in a UTF-8-compatible codepage on Windows. This fixes many
286 Unicode-rendering issues on Windows (e.g., error messages stating
287 `commitBuffer: invalid argument (invalid character)`).
289+ Idris now has a `--warnipkg` flag to enable auditing of Idris
290 packages during build time. Currently auditing check's the list of
291 modules specified in the `iPKG` file with those presented in the
296+ Terminating programs has been improved with more appropriate
297 functions (`exitWith`, `exitFailure`, and `exitSuccess`) and a data
298 structure (`ExitCode`) to capture a program's return code.
299+ Casting a `String` to an `Int`, `Integer` or a `Double` now ignores leading
300 and trailing whitespace. Previously only leading whitespace was ignored.
301+ RTS functions `openFile`, `do_popen`, and `ARGV` are now properly encoded using UTF-8 on Windows.
307* `record` syntax now allows updating fields, including nested fields,
308 by applying a function using the `$=` operator. For example:
316 record GameState where
317 constructor MkGameState
321 correct : GameState -> GameState
322 correct st = record { score->correct $= (+1),
323 score->attempted $= (+1) } st
326* Implicit parameter to interfaces are now allowed. For example:
329 interface Shows (ts : Vect k Type) where
330 shows : HVect ts -> Vect k String
332 In this interface, `k` is an implicit parameter, but previously needed to
338* The File Effect has been updated to take into account changes in
339 `Prelude.File` and to provide a 'better' API.
340* `natEnumFromThen` and `natEnumFromTo` have been updated to correctly calculate reverse ranges. Range syntax `[a,b..c]` now can be used again to generate reverse ranges.
341* `divBN` and `modBN` now can only be used for unsigned numbers.
342* `return`, which has been an alias for `pure` for many releases, is now deprecated.
343* Replace instance with implementation:
344 + `InstanceN` is deprecated, use `ImplementationN` instead.
345 + `InstanceCtorN` is deprecated, use `ImplementationCtorN` instead.
346 + `addInstance` is deprecated, use `addImplementation` instead.
347 + `%instance` keyword is deprecated, use `%implementation` instead.
349* Idris packages are now installed within a sub-directory `libs` of Idris' data directory, before they were installed in the directory's root.
353* Idris' documentation system now displays the documentation for auto
354 implicits in the output of `:doc`. This is tested for in `docs005`.
355* New command line flag `--info` that displays information about the installation.
356* New command line flag `--sourcepath <dir>` that allows adding directories to the source search path.
357* Allow 'installation' of a package's IdrisDoc documentation into a central location. The default location is the subdirectory `docs` of Idris' data directory.
358 * New flag `--installdoc <ipkg>` provided to install documentation
359 * New flag `--docdir` provided to show default documentation installation location.
360 * New environment variable `IDRIS_DOC_PATH` to allow specification of an alternative installation path for documentation.
361* Semantic meaning behind several environment variables has been clarified in documentation and code. See compilation section of the reference manual for more details.
362* Interface parameter constraints are now printed in the output of `:doc`. This
363 is tested for in `docs006`.
365## Miscellaneous updates
367* New, faster, better, implementation of the coverage checker
368* The test suite now uses [tasty-golden](https://hackage.haskell.org/package/tasty-golden). New tests must be registered in `test/TestData.hs`, as explained in the relevant `README.md`.
369* Added OSX and Windows continous integration with Travis and Appveyor.
373* The :e command can now handle an $EDITOR with arguments in it, like "emacs -nw"
380* `rewrite` can now be used to rewrite equalities on functions over
382* `rewrite` can now be given an optional rewriting lemma, with the syntax
383 `rewrite [rule] using [rewrite_lemma] in [scope]`.
385* Reorganised elaboration of `implementation`, so that interfaces with
386 dependencies between methods now work more smoothly
388* Allow naming of parent implementations when defining an implementation.
392 [PlusNatSemi] Semigroup Nat where
395 [MultNatSemi] Semigroup Nat where
398 -- use PlusNatSemi as the parent implementation
399 [PlusNatMonoid] Monoid Nat using PlusNatSemi where
402 -- use MultNatSemi as the parent implementation
403 [MultNatMonoid] Monoid Nat using MultNatSemi where
407* Interface definitions can now include data declarations (but not data
408 definitions). Any implementation of the interface must define the method
409 using a data type. The effect is to cause Idris to treat the method as
410 a data type (for unification and interface resolution purposes).
412* Experimentally, allow named implementations to be available by default in a
413 block of declarations with `using` notation. For example:
416 using implementation PlusNatMonoid
418 test x = x <+> x <+> neutral
421* Constraint arguments can now appear anywhere in function types, not just
422 at the top level or after an implicit argument binding.
424* Experimental extended `with` syntax, which allows calling functions defined
425 in a with block directly. For example:
428 data SnocList : List a -> Type where
430 Snoc : SnocList xs -> SnocList (xs ++ [x])
432 snocList : (xs : List a) -> SnocList a
434 my_reverse : List a -> List a
435 my_reverse xs with (snocList xs)
436 my_reverse [] | Empty = []
437 my_reverse (ys ++ [x]) | (Snoc p) = x :: my_reverse ys | p
440 The `| p` on the right hand side means that the `with` block function will
441 be called directly, so the recursive structure of `SnocList` can direct the
442 recursion structure of `my_reverse`.
444* Added `%fragile` directive, which gives a warning and a message when a
445 fragile name is referenced. For use in detailing fragile APIs.
447* The totality checker now looks under `case` blocks, rather than treating
448 them as mutually defined functions with their top level function, meaning
449 that it can spot more total functions.
451* The totality checker now looks under `if...then...else` blocks when checking
454* The `%assert_total` directive is now deprecated. Instead, you can
455 use one of the functions `assert_total`, `assert_smaller` or
456 `assert_unreachable` to describe more precisely where a totality assertion
461* `Control.WellFounded` module removed, and added to the Prelude as
462 `Prelude.WellFounded`.
463* Added `Data.List.Views` with views on `List` and their covering functions.
464* Added `Data.Nat.Views` with views on `Nat` and their covering functions.
465* Added `Data.Primitives.Views` with views on various primitive types and their covering functions.
466* Added `System.Concurrency.Sessions` for simple management of conversations
471* Taking cues from cabal, the `iPKG` format has been extended to
472 include more package metadata information. The following fields
475 + `brief`: Brief description of the package.
476 + `version`: Version string to associate with the package.
477 + `readme`: Location of the README file.
478 + `license`: Description of the licensing information.
479 + `author`: Author information.
480 + `maintainer`: Maintainer information.
481 + `homepage`: Website associated with the package.
482 + `sourcepage`: Location of the DVCS where the source can be found.
485## Miscellaneous updates
487* The Idris man page is now installed as part of the cabal/stack build process.
489* Improved startup performance by reducing the processing of an already imported
490 module that has changed accessibility.
492* A limited set of command line options can be used to override
493 package declared options. Overridable options are currently, logging
494 level and categories, default totality check, warn reach, IBC output
495 folder, and idris path. Note overriding IBC output folder, only
496 affects the installation of Idris packages.
498* Remove deprecated options `--ideslave` and `--ideslave-socket`. These options
499 were replaced with `--ide-mode` and `--ide-mode-socket` in 0.9.17
501* The code generator output type `MavenProject` was specific to the
502 Java codegen and has now been deprecated, together with the
503 corresponding `--mvn` option.
505* Definitional equality on Double is now bit-pattern identity rather
506 than IEEE's comparison operator. This prevents a bug where programs
507 could distinguish between -0.0 and 0.0, but the type theory could
508 not, leading to a contradiction. The new fine-grained equality
511* Naming conventions for Idris packages in an iPKG file now follow the
512 same rules for executables. Unquoted names must be valid namespaced
513 Idris identifiers e.g. ``package my.first.package``. Quoted package
514 names allow for packages to be given valid file names, for example,
515 ``package "my-first-package"``.
519* The implicit coercion from String to TTName was removed.
521* Decidable equality for TTName is available.
525## Updated export rules
527* The export rules are:
528 - 'private' means that the definition is not exported at all
529 - 'export' means that the top level type is exported, but not the
530 definition. In the case of 'data', this means the type constructor is
531 exported but not the data constructors.
532 - 'public export' means that the entire definition is exported.
533* By default, names are 'private'. This can be altered with an %access directive
535* Exported types can only refer to other exported names
536* Publicly exported definitions can only refer to publicly exported names
540* Idris functions can now be passed as callbacks to C functions or wrapped in a
542* C function pointers can be called.
543* Idris can access pointers to C globals.
547* Effects can now be given in any order in effect lists (there is no need for
548 the ordering to be preserved in sub lists of effects)
550## Elaborator reflection updates
552* Datatypes can now be defined from elaborator reflection:
553 - declareDatatype adds the type constructor declaration to the context
554 - defineDatatype adds the constructors to the datatype
555 - To declare an inductive-recursive family, declare the types of the function
556 and the type constructor before defining the pattern-match cases and
559## Minor language changes
561* The `[static]` annotation is changed to `%static` to be consistent with the
563* Added `%auto_implicits` directive. The default is `%auto_implicits on`.
564 Placing `%auto_implicits off` in a source file means that after that point,
565 any implicit arguments must be bound, e.g.:
568 append : {n,m,a:_} -> Vect n a -> Vect m a -> Vect (n + m) a
571 Only names which are used explicitly in the type need to be bound, e.g.:
574 Here : {x, xs : _} -> Elem x (x :: xs)
577 In `Here`, there is no need to bind any of the variables in the type of `xs`
578 (it could be e.g. `List a` or `Vect n a`; `a` and `n` will still be implicitly
581 You can still implicitly bind with 'using':
584 using (xs : Vect _ _)
585 data Elem : {a, n : _} -> a -> Vect n a -> Type where
586 Here : {x : _} -> Elem x (x :: xs)
587 There : {x, y : _} -> Elem x xs -> Elem x (y :: xs)
590 However, note that *only* names which appear in *both* the using block
591 *and* the type being defined will be implicitly bound. The following will
592 therefore fail because 'n' isn't implicitly bound:
595 using (xs : Vect n a)
596 bad : Elem x xs -> Elem x (y :: xs)
599* `Sigma` has been renamed to `DPair`.
600* Accessor functions for dependent pairs have been renamed to bring them into
601 line with standard accessor functions for pairs. The function `getWitness` is
602 now `fst`, and `getProof` is `snd`.
603* File Modes expanded: Append, ReadWriteTruncate, and ReadAppend added, Write is
604 deprecated and renamed to WriteTruncate.
605* C11 Extended Mode variations added to File Modes.
606* More flexible holes. Holes can now depend on other holes in a term (such as
607 implicit arguments which may be inferred from the definition of the hole).
608* Programs with holes can now be compiled. Attempting to evaluate an expression
609 with a hole results in a run time error.
610* Dependent pairs now can be specified using a telescope-style syntax, without
611 requirement of nesting, e.g. it is possible to now write the following:
614 (a : Type ** n : Nat ** Vect n a)
617* Idris will give a warning if an implicit is bound automatically, but would
618 otherwise be a valid expressio if the name was used as a global
620## External Dependencies
622* Curses has been removed as an external dependency.
626* `class` and `instance` are now deprecated keywords. They have been replaced by
627 `interface` and `implementation` respectively. This is to properly reflect
629* `(/)` operator moved into new Fractional interface.
630* Idris' logging infrastructure has been categorised. Command line and repl are
631 available. For command line the option `--logging-categories CATS` is used to
632 pass in the categories. Here `CATS` is a colon separated quoted string
633 containing the categories to log. The REPL command is `logcats CATS`. Where
634 `CATS` is a whitespace separated list of categoriese. Default is for all
635 categories to be logged.
636* New flag `--listlogcats` to list logging categories.
642* Improved unification by implementing a pattern unification rule
643* The syntax `` `{{n}}`` quotes n without resolving it, allowing short syntax for
644 defining new names. `` `{n}`` still quotes n to an existing name in scope.
645* A new primitive operator `prim__strSubstr` for more efficient extraction of
646 substrings. External code generators should implement this.
647* The previous syntax for tactic proofs and the previous interactive prover are
648 now deprecated in favour of reflected elaboration. They will be removed at
649 some point in the future.
650* Changed scoping rules for unbound implicits: any name which would be a valid
651 unbound implicit is now *always* an unbound implicit. This is much more
652 resilient to changes in inputs, but does require that function names be
653 explicitly qualified when in argument position.
654* Name binding in patterns follows the same rule as name binding for implicits
655 in types: names which begin with lower case letters, not applied to any
656 arguments, are treated as bound pattern variables.
657* Added `%deprecate` directive, which gives a warning and a message when a
658 deprecated name is referenced.
662* The `Neg` class now represents numeric types which can be negative. As such,
663 the `(-)` operator and `abs` have been moved there from `Num`.
664* A special version of `(-)` on `Nat` requires that the second argument is
665 smaller than or equal to the first. `minus` retains the old behaviour,
666 returning `Z` if there is an underflow.
667* The `(+)`, `(-)`, and `(*)` operations on Fin have been removed.
668* New Logging Effects have been added to facilitate logging of effectful
670* Elaborator reflection is now a part of the prelude. It is no longer necessary
671 to import `Language.Reflection.Elab`.
672* The `PERF` effect allows for simple performance metrics to be collected from
674* Some constructors that never actually occurred have been removed from the `TT`
675 and `Raw` reflection datatypes in Language.Reflection.
676* File `IO` operations (for example openFile/fread/fwrite) now return
677 `Either FileError ty` where the return type was previously `ty` to indicate
682* Records are now shown as records in `:doc`, rather than as the underlying
684* iPKG files have a new option `pkgs` which takes a comma-separated list of
685 package names that the idris project depends on. This reduces bloat in the
686 `opts` option with multiple package declarations.
687* iPKG files now allow `executable = "your filename here"` in addition to the
688 Existing `Executable = yourFilenameHere` style. While the unquoted version is
689 limited to filenames that look like namespaced Idris identifiers
690 (`your.filename.here`), the quoted version accepts any valid filename.
691* Add definition command (`\d` in Vim, `Ctrl-Alt-A` in Atom, `C-c C-s` in Emacs)
692 now adds missing clauses if there is already a definition.
694## Miscellaneous updates
696* Disable the deprecation warnings for %elim and old-style tactic scripts with
697 the `--no-elim-deprecation-warnings` and `--no-tactic-deprecation-warnings`
702* The Idris Reference manual has been fleshed out with content originally found
704* The `Show` class has been moved into `Prelude.Show` and augmented with the
705 method `showPrec`, which allows correct parenthesization of showed terms. This
706 comes with the type `Prec` of precedences and a few helper functions.
707* New REPL command `:printerdepth` that sets the pretty-printer to only descend
708 to some particular depth when printing. The default is set to a high number to
709 make it less dangerous to experiment with infinite structures. Infinite depth
710 can be set by calling :printerdepth with no argument.
711* Compiler output shows applications of `>>=` in do-notation
712* `fromInteger i` where `i` is an integer constant is now shown just as `i` in
714* An interactive shell, similar to the prover, for running reflected elaborator
715 actions. Access it with `:elab` from the REPL.
716* New command-line option `--highlight` that causes Idris to save highlighting
717 information when successfully type checking. The information is in the same
718 format sent by the IDE mode, and is saved in a file with the extension ".idh".
719* Highlighting information is saved by the parser as well, allowing it to
720 highlight keywords like `case`, `of`, `let`, and `do`.
721* Use predicates instead of boolean equality proofs as preconditions on `List`
723* More flexible 'case' construct, allowing each branch to target different
724 types, provided that the case analysis does not affect the form of any
725 variable used in the right hand side of the case.
726* Some improvements in interactive editing, particularly in lifting out
727 definitions and proof search.
728* Moved `System.Interactive`, along with `getArgs` to the Prelude.
729* Major improvements to reflected elaboration scripts, including the ability to run
730 them in a declaration context and many bug fixes.
731* `decl syntax` rules to allow syntax extensions at the declaration level
732* Experimental Windows support for console colours
736* GHC 7.10 compatibility
737* Add support for bundled toolchains.
738* Strings are now UTF8 encoded in the default back end
739* Idris source files are now assumed to be in UTF8, regardless of locale
741* Some reorganisation of primitives:
742 + `Buffer` and `BitVector` primitives have been removed (they were not tested
743 sufficiently, and lack a maintainer)
744 + `Float` has been renamed `Double` (`Float` is defined in the Prelude for
746 + Externally defined primitives and operations now supported with `%extern`
747 directive, allowing back ends to define their own special purpose primitives
748 + `Ptr` and `ManagedPtr` have been removed and replaced with external primitives
749* Add `%hint` function annotation, which allows functions to be used as hints in
750 proof search for `auto` arguments. Only functions which return an instance of
751 a data or record type are allowed as hints.
752* Syntax rules no longer perform variable capture. Users of effects will need to
753 explicitly name results in dependent effect signatures instead of using the
754 default name `result`.
755* Pattern-matching lambdas are allowed to be impossible. For example,
756 `Dec (2 = 3)` can now be constructed with `No $ \(Refl)` impossible, instead of
757 requiring a separate lemma.
758* Case alternatives are allowed to be impossible:
761 case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
764* The default `Semigroup` and `Monoid` instances for Maybe are now prioritised
765 choice, keeping the first success as Alternative does. The version that
766 collects successes is now a named instance.
767* `:exec` REPL command now takes an optional expression to compile and run/show
768* The return types of `Vect.findIndex`, `Vect.elemIndex` and `Vect.elemIndexBy`
769 were changed from `Maybe Nat` to `Maybe (Fin n)`
770* A new `:browse` command shows the contents of a namespace
771* `` `{n}`` is syntax for a quotation of the reflected representation
772 of the name `n`. If `n` is lexically bound, then the resulting
773 quotation will be for it, whereas if it is not, then it will succeed
774 with a quotation of the unique global name that matches.
775* New syntax for records that closely matches our other record-like structures:
776 type classes. See the updated tutorial for details.
777* Records can be coinductive. Define coinductive records with the `corecord`
779* Type class constructors can be assigned user-accessible names. This is done
780 using the same syntax as record constructors.
781* `if ... then ... else ...` is now built-in syntax instead of being defined in
782 a library. It is shown in REPL output and error messages, rather than its
784* The desugaring of `if ... then ... else ...` has been renamed to `ifThenElse`
785 from `boolElim`. This is for consistency with GHC Haskell and
786 scala-virtualized, and to reflect that if-notation makes sense with non-Bool
788* Agda-style semantic highlighting is supported over the IDE protocol.
789* Experimental support for elaborator reflection. Users can now script the
790 elaborator, for use in code generation and proof automation. This feature is
791 still under rapid development and is subject to change without notice. See
792 Language.Reflection.Elab and the %runElab constructs
796* The `--ideslave` command line option has been replaced with a `--ide-mode`
797 command line option with the same semantics.
798* A new tactic `claim N TY` that introduces a new hole named `N` with type `TY`
799* A new tactic `unfocus` that moves the current hole to the bottom of the
801* Quasiquotation supports the generation of `Language.Reflection.Raw` terms in
802 addition to `Language.Reflection.TT`. Types are used for disambiguation,
803 defaulting to `TT` at the REPL.
804* `Language.Reflection.Quotable` now takes an extra type parameter which
805 determines the type to be quoted to. Instances are provided to quote common
806 types to both `TT` and `Raw`.
807* Library operators have been renamed for consistency with Haskell. In
808 particular, `Applicative.(<$>)` is now `Applicative.(<*>)` and `(<$>)` is now
809 an alias for Functor.map. Correspondingly, ($>) and (<$) have been renamed to
810 `(<*)` and `(*>)`. The cascading effects of this rename are that
811 `Algebra.(<*>)` has been renamed to `Algebra.(<.>)` and `Matrix.(<.>)` is now
813* Binding forms in DSL notation are now given an extra argument: a reflected
814 representation of the name that the user chose. Specifically, the rewritten
815 `lambda`, `pi`, and `let` binders will now get an extra argument of type
816 `TTName`. This allows more understandable dynamic errors in DSL code and more
817 readable code generation results.
818* DSL notation can now be applied with `$`
819* Added `FFI_Export` type which allows Idris functions to be exportoed and
820 called from foreign code
821* Instances can now have documentation strings.
822* Type providers can have documentation strings.
823* Unification errors now (where possible) contain information about provenance
825* New REPL command `:core TM` that shows the elaborated form of `TM` along with
826 its elaborated type using the syntax of `TT`. IDE mode has a corresponding
827 command `:elaborate-term` for serialized terms.
828* Effectful and IO function names for sending data to STDOUT have been
829 aligned, semantically.
830 + `print` is now for putting showable things to STDOUT.
831 + `printLn` is for putting showable things to STDOUT with a new line
832 + `putCharLn` for putting a single character to STDOUT, with a new line.
833* Classes can now be annotated with 'determining parameters' to say which must
834 be available before resolving instances. Only determining parameters are
835 checked when checking for overlapping instances.
836* New package `contrib` containing things that are less mature or less used than
837 the contents of `base`. `contrib` is not available by default, so you may need
838 to add `-p contrib` to your .ipkg file or Idris command line.
839* Arguments to class instances are now checked for injectivity. Unification
840 assumes this, so we need to check when instances are defined.
844* Inductive-inductive definitions are now supported (i.e. simultaneously defined
845 types where one is indexed by the other.)
846* Implicits and type class constraints can now appear in scopes other than the
848* Importing a module no longer means it is automatically reexported. A new
849 `public` modifier has been added to import statements, which will reexport the
850 names exported from that module.
851* Implemented `@`-patterns. A pattern of the form `x@p` on the left hand side
852 matches `p`, with `x` in scope on the right hand side with value `p`.
853* A new tactic sourceLocation that fills the current hole with the current
854 source code span, if this information is available. If not, it raises an
856* Better Unicode support for the JavaScript/Node codegen
857* `:search` and `:apropos` commands can now be given optional package lists to
859* `Vect`, `Fin` and `So` moved out of prelude into `base`, in modules
860 `Data.Vect`, `Data.Fin` and `Data.So` respectively.
861* Several long-standing issues resolved, particularly with pattern matching and
863* Modules can now have API documentation strings.
867* Two new tactics: `skip` and `fail`. Skip does nothing, and fail takes a string
868 as an argument and produces it as an error.
869* Corresponding reflected tactics `Skip` and `Fail`. Reflected `Fail` takes a
870 list of `ErrorReportParts` as an argument, like error handlers produce,
871 allowing access to the pretty-printer.
872* Stop showing irrelevant and inaccessible internal names in the interactive
874* The proof arguments in the `List` library functions are now implicit and
875 solved automatically.
876* More efficient representation of proof state, leading to faster elaboration of
878* *EXPERIMENTAL* Implementation of uniqueness types
879* Unary negation now desugars to `negate`, which is a method of the `Neg` type
880 class. This allows instances of `Num` that can't be negative, like `Nat`, and
881 it makes correct IEEE Float operations easier to encode. Additionally, unary
882 negation is now available to DSL authors.
883* The Java and LLVM backends have been factored out for separate
884 maintenance. Now, the compiler distribution only ships with the C and
886* New REPL command `:printdef` displays the internal definition of a name
887* New REPL command `:pprint` pretty-prints a definition or term with LaTeX or
889* Naming of data and type constructors is made consistent across the standard
891* Terms in `code blocks` inside of documentation strings are now parsed and type
892 checked. If this succeeds, they are rendered in full color in documentation
893 lookups, and with semantic highlighting for IDEs.
894* Fenced code blocks in docs defined with the "example" attribute are rendered
896* Fenced code blocks declared to be Idris code that fail to parse or type check
897 now provide error messages to IDE clients.
898* *EXPERIMENTAL* support for partial evaluation (Scrapping your Inefficient
903* Tactic for case analysis in proofs
904* Induction and case tactic now work on expressions
905* Support for running tests for a package with the tests section of .ipkg files
906 and the `--testpkg` command-line option
907* Clearly distinguish between type providers and postulate providers at the use
909* Allow dependent function syntax to be overridden in dsl blocks, similarly to
910 functions and let. The keyword for this is `pi`.
911* Updated `effects` library, with simplified API
912* All new JavaScript backend (avoids callstack overflows)
913* Add support for `%lib` directive for NodeJS
914* Quasiquotes and quasiquote patterns allow easier work with reflected
915 terms. `` `(EXPR)`` quasiquotes EXPR, causing the elaborator to be
916 used to produce a reflected version of it. Subterms prefixed with `~`
917 are unquoted - on the RHS, they are reflected terms to splice in,
918 while on the LHS they are patterns.
920 A quasiquote expression can be given a goal type for the elaborator,
921 which helps with disambiguation. For instance, `` `(() : ())``
922 quotes the unit constructor, while `` `(() : Type)`` quotes the unit
923 type. Both goal types and quasiquote are typechecked in the global
925* Better inference of unbound implicits
929* IDE support for retrieving structured information about metavariables
930* Experimental Bits support for JavaScript
931* IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
932* Command line option `-e` (or `--eval`) to evaluate expressions without loading
933 the REPL. This is useful for writing more portable tests.
934* Many more of the basic functions and datatypes are documented.
935* Primitive types such as Int and String are documented
936* Removed javascript lib in favor of idris-hackers/iQuery
937* Specify codegen for :compile REPL command (e.g. `:compile` javascript
939* Remove `:info` REPL command, subsume and enhance its functionality in the `:doc` command
940* New (first class) nested record update/access syntax:
943 record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val
944 record { a->b->c } x -- accesses field, equivalent to c (b (a x))
947* The banner at startup can be suppressed by adding `:set` nobanner to the initialisation script.
948* `:apropos` now accepts space-delimited lists of query items, and searches for
949 the conjunction of its inputs. It also accepts binder syntax as search
950 strings - for instance, `->` finds functions.
951* Totality errors are now treated as warnings until code generation time, when
952 they become errors again. This allows users to use the interactive editing
953 features to fix totality issues, but no programs that violate the stated
954 assumptions will actually run.
955* Added `:makelemma` command, which adds a new top level definition to solve a
957* Extend `:addclause` to add instance bodies as well as definitions
958* Reverse parameters to `BoundedList` -- now matches `Vect`, and is easier to
960* Move `foldl` into Foldable so it can be overridden.
961* Experimental `:search` REPL command for finding functions by type
965* New implementation of erasure
969* Proof search now works for metavariables in types, giving some interactive
971* New `Lazy` type, replacing laziness annotations.
972* JavaScript and Node codegen now understand the `%include` directive.
973* Concept of `null` is now understood in the JavaScript and Node codegen.
974* Lots of performance patches for generated JavaScript.
975* New commands `:eval` (`:e`) and `:type` (`:t`) in the prover, which either
976 normalise or show the type of expressions.
977* Allow type providers to return postulates in addition to terms.
978* Syntax for dealing with match failure in `<-` and pattern matching let.
979* New syntax for inline documentation. Documentation starts with `|||`, and
980 arguments are documented by preceding their name with `@`. Example:
983 ||| Add two natural numbers
984 ||| @ n the first number (examined by the function)
985 ||| @ m the second number (not examined)
986 plus (n, m : Nat) -> Nat
989* Allow the auto-solve behaviour in the prover to be disabled, for easier
990 debugging of proof automation. Use `:set autosolve` and `:unset autosolve`.
991* Updated `effects` library
992* New `:apropos` command at REPL to search documentation, names, and types
993* Unification errors are now slightly more informative
994* Support mixed induction/coinduction with `Inf` type
995* Add `covering` function option, which checks whether a function and all
996 descendants cover all possible inputs
1000* Agda-style equational reasoning (in Syntax.PreorderReasoning)
1001* 'case' construct now abstracts over the scrutinee in its type
1002* Added label type 'name (equivalent to the empty type). This is intended for
1003 field/effect disambiguation. "name" can be any valid identifier. Two labels
1004 are definitionally equal if they have the same name.
1005* General improvements in error messages, especially %error_reverse annotation,
1006 which allows a hint as to how to display a term in error messages
1007* `--ideslave` mode now transmits semantic information about many of the strings
1008 that it emits, which can be used by clients to implement semantic highlighting
1009 like that of the REPL. This has been implemented in the Emacs mode and the IRC
1010 bot, which can serve as examples.
1011* New expression form: `with NAME EXPR` privileges the namespace `NAME` when
1012 disambiguating overloaded names. For example, it is possible to write `with
1013 Vect [1,2,3]` at the REPL instead of `the (Vect _ _) [1,2,3]`, because the
1014 `Vect` constructors are defined in a namespace called `Vect`.
1015* `assert_smaller` internal function, which marks an expression as smaller than
1016 a pattern for use in totality checking. e.g. `assert_smaller (x :: xs) (f
1017 xs)` asserts that `f xs` will always be structurally smaller than `(x :: xs)`
1018* `assert_total` internal function, which marks a subexpression as assumed to be
1019 total, e.g `assert_total (tail (x :: xs))`.
1020* Terminal width is automatically detected if Idris is compiled with curses
1021 support. If curses is not available, automatic mode assumes 80 columns.
1022* Changed argument order for `Prelude.Either.either`.
1023* Experimental `neweffects'`library, intended to replace `effects` in the next
1030* Pretty-printer now used for all term output
1034* Type classes now implemented as dependent records, meaning that method types
1035 may now depend on earlier methods.
1036* More flexible class instance resolution, so that function types and lambda
1037 expressions can be made instances of a type class.
1038* Add `!expr` notation for implicit binding of intermediate results in
1039 monadic/do/etc expressions.
1040* Extend Effects package to cope with possibly failing operations, using
1041 `if_valid`, `if_error`, etc.
1042* At the REPL, `it` now refers to the previous expression.
1043* Semantic colouring at the REPL. Turn this off with `--nocolour`.
1044* Some prettifying of error messages.
1045* The contents of `~/.idris/repl/init` are run at REPL start-up.
1046* The REPL stores a command history in `~/.idris/repl/history`.
1047* The `[a..b]`, `[a,b..c]`, `[a..]`, and `[a,b..]` syntax now pass the totality
1048 checker and can thus be used in types. The `[x..]` syntax now returns an
1049 actually infinite stream.
1050* Add `%reflection` option for functions, for compile-time operations on syntax.
1051* Add expression form `quoteGoal x by p in e` which applies `p` to the expected
1052 expression type and binds the result to `x` in the scope `e`.
1053* Performance improvements in Strings library.
1054* Library reorganisation, separated into `prelude/` and `base/`.
1058* New module/dependency tree checking.
1059* New parser implementation with more precise errors.
1060* Improved type class resolution.
1061* Compiling Nat via GMP integers.
1062* Performance improvements in elaboration.
1063* Improvements in termination checking.
1064* Various REPL commands to support interactive editing, and a client/server
1065 mode to allow external invocation of REPL commands.
1069## User visible changes
1071* Apply functions by return type, rather than with arguments: `t <== f` means
1072 "apply f with arguments such that it returns a value of type t"
1073* Allow the result type of a rewrite to be specified
1074* Allow names to be attached to provisional definitions lhs `?= {name} rhs` --
1075 generates a lemma called `name` which makes the types of the lhs and rhs
1076 match. `{name}` is optional - a unique name is generated if it is absent.
1077* Experimental LLVM backend
1078* Added `Data.HVect` module
1079* Fix `fromInteger` to take an `Integer`, rather than an `Int`
1080* Integer literals for `Fin`
1081* Renamed `O` to `Z`, and `fO` to `fZ`
1082* Swapped `Vect` arguments, now `Vect : Nat -> Type -> Type`
1083* Added `DecEq` instances
1084* Add `equiv` tactic, which rewrites a goal to an equivalent (convertible) goal
1088* Add annotation for unification traces
1089* Add `mrefine` tactic for refining by matching against a type
1090* Type class resolution fixes
1091* Much faster coverage checking
1095## User visible changes
1097* Added `rewrite ... in ...` construct
1098* Allow type class constraints in `using` clauses
1099* Renamed `EFF` to `EFFECT` in Effect package
1100* Experimental Java backend
1101* Tab completion in REPL
1102* Dynamic loading of C libraries in the interpreter
1103* Testing IO actions at the REPL with `:x` command
1104* Improve rendering of `:t`
1105* Fixed some INTERNAL ERROR messages
1109* Fix non-linear pattern checking
1110* Improved name disambiguation
1111* More flexible unification and elaboration of lambdas
1112* Various unification and totality checking bug fixes
1116## User visible changes
1118* `implicit` keyword, for implicit type conversion
1119* Added Effects package
1120* Primitives for 8,16,32 and 64 bit integers
1124* Change unification so that it keeps track of failed constraints in case
1125 later information helps to resolve them
1126* Distinguishing parameters and indices in data types
1127* Faster termination/coverage checking
1128* Split 'javascript' target into 'javascript' and 'node'
1132## User visible changes
1134* The type of types is now `Type` rather than `Set`
1135* Forward declarations of data allowed
1136 - supporting induction recursion and mutually recursive data
1137* Type inference of definitions in `where` clauses
1138 - Provided that the type can be completely determined from the first
1139 application of the function (in the top level definition)
1140* `mutual` blocks added
1141 - effect is to elaborate all types of declarations in the block before
1142 elaborating their definitions
1143 - allows inductive-recursive definitions
1144* Expression inspected by `with` clause now abstracted from the goal
1146* Implicit arguments will be added automatically only if their initial letter is
1147 lower case, or they are in a using declaration
1148* Added documentation comments (Haddock style) and `:doc` REPL command
1149* Pattern matching on strings, big integers and characters
1150* Added `System.Concurrency` modules
1151* Added `postulate` declarations
1152* Allow type annotations on `let` tactic
1153* EXPERIMENTAL JavaScript generation, with `--target javascript` option
1157* Separate inlining methods at compile-time and run-time
1158* Fixed nested parameters blocks
1159* Improve efficiency of elaborator by:
1160 - only normalising when necessary
1161 - reducing backtracking with resolving ambiguities
1162* Better compilation of case trees
1166## User visible changes
1169 - as data declarations, but constructor arguments are evaluated lazily
1170 - functions which return a codata type do not reduce at compile time
1171* Added `parameters` blocks
1172* Allow local data definitions in where blocks
1173* Added `%default` directive to declare total-by-default or partial-by-default
1174 for functions, and a corresponding "partial" reserved words to mark functions
1175 as allowed to be partial. Also `--total` and `--partial` added as command line
1177* Command line option `--warnpartial` for flagging all undeclared partial
1178 functions, without error.
1179* New termination checker supporting mutually recursive definitions.
1180* Added `:load` command to REPL, for loading a new file
1181* Added `:module` command to REPL, for adding modules
1182* Renamed library modules (now have initial capital)
1186* Several improvements and fixes to unification
1187* Added collapsing optimisation and more aggressive erasure
1191## User visible changes
1193* Simple packaging system
1194* Added `--dumpc` flag for displaying generated code
1198* Improve overloading resolution (especially where this is a type error)
1199* Various important bug fixes with evaluation and compilation
1200* More aggressive compile-time evaluation
1204## User visible changes
1206* Added binding forms to syntax rules
1207* Named class instances
1208* Added `:set` command, with options `errorcontext` for displaying local
1209 variables in scope when a unification error occurs, and `showimplicits`
1210 for displaying elaborated terms in full
1211* Added `--errorcontext` command line switch
1212* Added `:proofs` and `:rmproofs` commands
1213* Various minor REPL improvements and fixes
1217* Completely new run time system (not based on Epic or relying on Boehm GC)
1218* Normalise before forcing to catch more forceable arguments
1219* Types no longer exported in normal form
1220* Try to resolve overloading by inspecting types, rather than full type
1225## User visible changes
1227* backtick notation added: ``x `foo` y ==> foo x y``
1228* case expressions allowed in type signatures
1229* Library extensions in prelude.vect and prelude.algebra
1230* `malloc`/`trace_malloc` added to builtins.idr
1234* Some type class resolution fixes
1235* Several minor bug fixes
1236* Performance improvements in resolving overloading and type classes
1240## User visible changes
1242* DSL notation, for overloading lambda and let bindings
1243* Dependent records, with projection and update
1244* Totality checking and `total` keyword
1245* Auto implicits and default argument values `{auto n : T}`, `{default val n : T}`
1246* Overlapping type class instances disallowed
1247* Many extensions to `prelude.nat` and `prelude.list` libraries (mostly thanks to
1249* New libraries: `control.monad.identity`, `control.monad.state`
1250* Small improvements in error reporting
1254* Faster compilation (only compiling names which are used)
1255* Better type class resolution
1256* Lots of minor bug fixes
1262## User visible changes
1264* New proof/tactics syntax
1265* New syntax for pairs/dependent pairs
1266* Indentation-significant syntax
1268* Added where clauses
1269* Added case expressions, pattern matching let and lambda
1270* Added monad comprehensions
1271* Added cumulativity and universe checking
1272* Ad-hoc name overloading
1273 - Resolved by type or explicit namespace
1274* Modules (Haskell-style)
1275* public, abstract and private access to functions and types
1276* Separate type-checking
1277* Improved interactive environment
1278* Replaced 'do using' with Monad class
1279* Extended syntax macros
1284* All definitions (functions, classes and instances) are elaborated to top
1285 level, fully explicit, data declarations and pattern matching definitions,
1286 which are verified by a minimal type checker.
1288This is the first release of a complete reimplementation. There will be bugs.
1289If you find any, please do not hesitate to contact Edwin Brady
1290(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