mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
A bit of shuffling in the CHANGEGLOG
This commit is contained in:
parent
6494241c11
commit
b6a3c51129
34
CHANGELOG.md
34
CHANGELOG.md
@ -5,21 +5,12 @@ The implementation is now self-hosted. To initialise the build, either use
|
||||
the [bootstrapping version of Idris2](https://github.com/edwinb/Idris2-boot)
|
||||
or build from the generated Scheme, using `make bootstrap`.
|
||||
|
||||
Compiler updates:
|
||||
|
||||
* Data types with a single constructor, with a single unerased arguments,
|
||||
are translated to just that argument, to save repeated packing and unpacking.
|
||||
(c.f. `newtype` in Haskell)
|
||||
+ A data type can opt out of this behaviour by specifying `noNewtype` in its
|
||||
options list. `noNewtype` allows code generators to apply special handling
|
||||
to the generated constructor/deconstructor, for a newtype-like data type,
|
||||
that would otherwise be optimised away.
|
||||
* 0-multiplicity constructor arguments are now properly erased, not just
|
||||
given a placeholder null value.
|
||||
|
||||
Language changes:
|
||||
|
||||
* `total`, `covering` and `partial` flags on functions now have an effect.
|
||||
* Fields of records can be accessed (and updated) using the dot syntax,
|
||||
such as `r.field1.field2` or `record { field1.field2 = 42 }`.
|
||||
For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
|
||||
* %transform directive, for declaring transformation rules on runtime
|
||||
expressions. Transformation rules are automatically added for top level
|
||||
implementations of interfaces.
|
||||
@ -34,22 +25,27 @@ Library additions:
|
||||
* New modules in `contrib` for JSON (`Language.JSON.*`); random numbers
|
||||
(`System.Random`)
|
||||
|
||||
Compiler updates:
|
||||
|
||||
* Data types with a single constructor, with a single unerased arguments,
|
||||
are translated to just that argument, to save repeated packing and unpacking.
|
||||
(c.f. `newtype` in Haskell)
|
||||
+ A data type can opt out of this behaviour by specifying `noNewtype` in its
|
||||
options list. `noNewtype` allows code generators to apply special handling
|
||||
to the generated constructor/deconstructor, for a newtype-like data type,
|
||||
that would otherwise be optimised away.
|
||||
* 0-multiplicity constructor arguments are now properly erased, not just
|
||||
given a placeholder null value.
|
||||
|
||||
Other improvements:
|
||||
|
||||
* Various performance improvements in the typechecker:
|
||||
+ Noting which metavariables are blocking unification constraints, so that
|
||||
they only get retried if those metavariables make progress.
|
||||
+ Evaluating `fromInteger` at compile time.
|
||||
+ In the run-time, reuse the old heap after garbage collection if it
|
||||
hasn't been resized, to avoid unnecessary system calls.
|
||||
|
||||
* Extend Idris2's literate mode to support reading Markdown and OrgMode files.
|
||||
For more details see: https://idris2.readthedocs.io/en/latest/reference/literate.html
|
||||
|
||||
* Fields of records can be accessed (and updated) using the dot syntax,
|
||||
such as `r.field1.field2` or `record { field1.field2 = 42 }`.
|
||||
For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
|
||||
|
||||
Changes since Idris 1
|
||||
---------------------
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user