Idris2/CHANGELOG.md

Changes since Idris 2 v0.2.0

Language changes:

• Bits8, Bits16, Bits32 and Bits64 primitive types added, with:
  • Num, Eq, Ord and Show implementations.
  • Casts from Integer, for literals
  • Casts to Int (except Bits64 which might not fit), Integer and String
  • Passed to C FFI as unsigned
  • Primitives added in Data.Buffer
• Elaborator reflection and quoting terms
  • Requires extension %language ElabReflection
  • API defined in Language.Reflection, including functions for getting types of global names, constructors of data types, and adding new top level declarations
  • Implemented %macro function flag, to remove the syntactic noise of invoking elaborator scripts. This means the function must always be fully applied, and is run under %runElab

Library changes:

• Experimental Data.Linear.Array added to contrib, support mutable linear arrays with constant time read/write, convertible to immutable arrays with constant time read.
  • Anything in Data.Linear in contrib, just like the rest of contrib, should be considered experimental with the API able to change at any time! Further experiments in Data.Linear are welcome :).

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.
• %default <totality status> has been implemented. By default, functions must be at least covering
  • That is, %default covering is the default status.
• 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)
• To improve error messages, one can use with NS.name <term> or with [NS.name1, NS.name2, ...] <term> to disable disambiguation for the given names in <term>. Example: with MyNS.(>>=) do ....

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