idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-15 22:32:19 +03:00
Code Issues Projects Releases Wiki Activity
e30f7ef3ed
Idris2/CHANGELOG.md
Edwin Brady a5c2c211a1 Add %tcinline flag to high level syntax 
This allows a function to be inlined for totality checking purposes
only. So, for example, (>>=) might be a function, but if it evaluates to
something constructor guarded in some context, then it might still be
productive.
2020-05-22 16:01:47 +01:00

2.5 KiB
Raw Blame History

Changes since Idris 2 v0.1.0

The implementation is now self-hosted. To initialise the build, either use the bootstrapping version of Idris2 or build from the generated Scheme, using make bootstrap.

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
  • New function flag %tcinline which means that the function should be inlined for the purposes of totality checking (but otherwise not inlined). This can be used as a hint for totality checking, to make the checker look inside functions that it otherwise might not.
  • %transform directive, for declaring transformation rules on runtime expressions. Transformation rules are automatically added for top level implementations of interfaces.
  • A %spec flag on functions which allows arguments to be marked for partial evaluation, following the rules from "Scrapping Your Inefficient Engine" (ICFP 2010, Brady & Hammond)

Library additions:

  • Additional file management operations in base
  • New module in base for time (System.Clock)
  • 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.
  • 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

Changes since Idris 1

Everything :). For full details, see: https://idris2.readthedocs.io/en/latest/updates/updates.html