Changelog History
-
v2.6.3 Changes
Highlights
β Added support for Erased Cubical Agda, a variant of Cubical Agda that is supported by the GHC backend, under the flag
--erased-cubical
.β Added a new flag
--cubical-compatible
to turn on generation of Cubical Agda-specific support code (previously this behaviour was part of--without-K
).
Since
--cubical-compatible
mode implies that functions should work with the preliminary support for indexed inductive types in Cubical Agda, many pattern matching functions will now emit anUnsupportedIndexedMatch
warning, indicating that the function will not compute when applied to transports (from--cubical
code).This warning can be disabled with
-WnoUnsupportedIndexedMatch
, which can be used either in anOPTIONS
pragma or in youragda-lib
file. The latter is recommended if your project is only--cubical-compatible
, or if it is already making extensive use of indexed types.π New primitives
declareData
,defineData
, andunquoteDecl data
for generating new data types have been added to the reflection API.π Thanks to a number of performance improvements, Agda 2.6.3 is about 30% faster than Agda 2.6.2.2 at type-checking the standard library with the
--without-K
flag, and 10% faster when using with the (new)--cubical-compatible
flag instead (some details can be found here).
Installation and infrastructure
π Agda supports GHC versions 8.0.2 to 9.4.3.
Erasure
- The new option
--erased-cubical
turns on a variant of Cubical Agda (see #4701).
When this variant of Cubical Agda is used glue (and some related builtins) may only be used in erased settings. One can import regular Cubical Agda code from this variant of Cubical Agda, but names defined using Cubical Agda are (mostly) treated as if they had been marked as erased. See the reference manual for more details.
The GHC backend can compile code that uses
--erased-cubical
if the top-level module uses this flag.This feature is experimental.
- The parameter arguments of constructors and record fields are now
marked as erased
(#4786), with one
exception: for indexed data types this only happens if the
--with-K
flag is active (#6297).
For instance, the type of the constructor
c
below is now{@0 A : Set} β D A
, and the type of the record fieldR.f
is{@0 A : Set} β R A β A
:data D (A : Set) : Set where c : D A record R (A : Set) : Set where field f : A
- β Added an option
--erase-record-parameters
that additionally marks parameters to definitions in a record module as erased (#5770). For example:
{-# OPTIONS --erase-record-parameters #-} postulate A : Set postulate a : A record R (x : A) : Set where y : A y = a f : (@0 x : A) β R x β A f x r = R.y {x} r
Cubical Agda
- π₯ [Breaking] The generation of Cubical Agda-specific support code was removed
from
--without-K
and transferred to its own flag,--cubical-compatible
(see #5843 and #6049 for the rationale).
Note that code that uses (only)
--without-K
can no longer be imported from code that uses--cubical
. Thus it may make sense to replace--without-K
with--cubical-compatible
in library code, if possible.Note also that Agda tends to be quite a bit faster if
--without-K
is used instead of--cubical-compatible
.Note finally that when
--without-K
is used it might not be safe to compile and run programs that postulate erased univalence (but we are currently not aware of a program that would go wrong).π Cubical Agda now has experimental support for indexed inductive types (#3733). See the user guide for caveats.
The cubical interval
I
now belongs to its own sort,IUniv
, rather thanSSet
. ForJ : IUniv
andA : J β Set l
, we have(j : J) β A j : Set l
, that is, the type of functions from a type inIUniv
to a fibrant type is fibrant.The option
--experimental-irrelevance
is now perhaps incompatible with Cubical Agda and perhaps also postulated univalence (see #5611 and #5861).
This is not meant to imply that the option was not already incompatible with those things. Note that
--experimental-irrelevance
cannot be used together with--safe
.- A new built-in constructor
REFLID
was added to the cubical identity types. This is definitionally equal to the reflexivity identification built withconid
, with the difference being that matching onREFLID
is allowed.
symId : β {a} {A : Set a} {x y : A} β Id x y β Id y x symId reflId = reflId
Definitions which pattern match on higher-inductive types are no longer considered for injectivity analysis. (#6219)
π₯ [Breaking] Higher constructors are no longer considered as guarding in the productivity check. (#6108)
π Rewrite rules with interval arguments are now supported. (#4384)
The flat modality
- π₯ [Breaking] The
@flat
/@β
modality is now by default disabled (see #4927).
It can be enabled using the infective flag
--cohesion
.- π₯ [Breaking] Matching on
@flat
arguments is now disabled by default, the flag--no-flat-split
has been removed, and the flag--flat-split
is now infective (see #6238 and #6263).
Matching can be enabled using the
--flat-split
flag. Note that in Cubical Agda functions that match on an argument marked with@flat
trigger theUnsupportedIndexedMatch
warning, and the code might not compute properly.Reflection
- Two new reflection primitives
declareData : Name β Nat β Type β TC β€ defineData : Name β List (Ξ£ Name (Ξ» _ β Type)) β TC β€
are added for declaring and defining datatypes, similar to
declareDef
anddefineDef
.- The construct
unquoteDecl
is extended with the ability of bringing a datatyped
and its constructorscβ ... cβ
given by aTC
computationm
into scope by the following syntax:
unquoteDecl data x constructor cβ .. cβ = m
A new reflection primitive
getInstances : Meta β TC (List Term)
was added toAgda.Builtin.Reflection
. This operation returns the list of all possibly valid instance candidates for a given metavariable. For example, the following macro instantiates the goal with the first instance candidate, even if there are several:macro pickWhatever : Term β TC β€ pickWhatever hole@(meta m _) = do (cand β· _) β getInstances m where [] -> typeError (strErr "No candidates!" β· []) unify hole cand pickWhatever _ = typeError (strErr "Already solved!" β· [])
π₯ [Breaking] The reflection primitives
getContext
andinContext
use a nominal contextList (Ξ£ String Ξ» _ β Arg Type)
instead ofList (Arg Type)
for printing type information better. Similarly,extendContext
takes an extra argument of typeString
.macro
definitions can now be used even when they are declared as erased. For example, this is now accepted:macro @0 trivial : Term β TC β€ trivial = unify (con (quote refl) [])
test : 42 β‘ 42 test = trivial
* A new reflection primitive `formatErrorParts : List ErrorPart β TC String` is added. It takes a list of `ErrorPart` and return its formatted string. * π₯ [**Breaking**] A new constructor `pattErr : Pattern β ErrorPart` of `ErrorPart` for reflection is added. * π₯ [**Breaking**] The reflection primitives `getType` and `getDefinition` respect the module context they are invoked from instead of returning information that would be expected in the top context. * π₯ [**Breaking**] The reflection primitive `inContext` cannot step outside of the context that the `TC` computation is invoked from anymore. The telescope is now relative to that context instead. Syntax ------ * It is now OK to put lambda-bound variables anywhere in the right-hand side of a syntax declaration. However, there must always be at least one "identifier" between any two regular "holes". For instance, the following syntax declaration is accepted because `-` is between the holes `B` and `D`. ```agda postulate F : (Set β Set) β (Set β Set) β Set syntax F (Ξ» A β B) (Ξ» C β D) = B A C - D
- Syntax can now use lambdas with multiple arguments (#394).
Example:
postulate Ξ£β : (A : Set) β (A β A β Set) β Set syntax Ξ£β A (Ξ» xβ xβ β P) = [ xβ xβ β¦ A ] Γ P
Builtins
- π₯ [Breaking] Change
primFloatToWord64
to returnMaybe Word64
. (See #6093.)
The new type is
primFloatToWord64 : Float β Maybe Word64
and it returns
nothing
forNaN
.π₯ [Breaking] The type expected by the builtin
EQUIVPROOF
has been changed to properly encode the condition thatEQUVIFUN
is an equivalence. (#5661, #6032)π₯ [Breaking] The primitive
primIdJ
has been removed (#6032) in favour of matching on the cubical identity type.π₯ [Breaking] The builtin
SUBIN
is now exported fromAgda.Builtin.Cubical.Sub
asinS
rather thaninc
. Similarly, the internal modules refer toprimSubOut
asoutS
. (#6032)
Pragmas and options
- It is now possible to declare several
BUILTIN REWRITE
relations. Example: ```agda {-# OPTIONS --rewriting #-}
open import Agda.Builtin.Equality open import Agda.Builtin.Equality.Rewrite -- 1st rewrite relation
postulate R : (A : Set) β A β A β Set A : Set a b c : A foo : R A a b -- using 2nd rewrite relation bar : b β‘ c -- using 1st rewrite relation
{-# BUILTIN REWRITE R #-} -- 2nd rewrite relation {-# REWRITE foo bar #-}
test : a β‘ c test = refl
* π₯ [**Breaking**] Option `--experimental-lossy-unification` that turns on (the incomplete) first-order unification has been renamed to `--lossy-unification`. ([#1625](https://github.com/agda/agda/issues/1625)) * The new option `--no-load-primitives` complements `--no-import-sorts` by foregoing loading of the primitive modules altogether. This option leaves Agda in a very fragile state, as the built-in sorts are used extensively throughout the implementation. It is intended to be used by Literate Agda projects which want to bind `BUILTIN TYPE` (and other primitives) in their own literate files. * If `--interaction-exit-on-error` is used, then Agda exits with a non-zero exit code if `--interaction` or `--interaction-json` are used and a type error is encountered. The option also makes Agda exit with exit code 113 if Agda fails to parse a command. This option might for instance be used if Agda is controlled from a script. * Add a `NOT_PROJECTION_LIKE` pragma, which marks a function as not suitable for projection-likeness. Projection-like functions have some of their arguments erased, which can cause confusing behaviour when they are printed instantiated (see [#6203](https://github.com/agda/agda/issues/6203)). * π₯ [**Breaking**] The options `--subtyping` and `--no-subtyping` have been removed (see [#5427](https://github.com/agda/agda/issues/5427)). π Profiling and performance ------------------------- * π New verbosity `-v debug.time:100` adds time stamps to debugging output. * π₯ [**Breaking**] Profiling options are now turned on with a new `--profile` flag instead of abusing the debug verbosity option. (See [#5781](https://github.com/agda/agda/issues/5781).) * The new profiling option `--profile=conversion` collects statistics on how often various steps of the conversion algorithm are used (reduction, eta-expansion, syntactic equality, etc). * Meta-variables can now be saved in `.agdai` files, instead of being expanded. This can affect performance. (See [#5731](https://github.com/agda/agda/issues/5731).) Meta-variables are saved if the pragma option `--save-metas` is used. This option can be overridden by `--no-save-metas`. * The new option `--syntactic-equality[=FUEL]` can be used to limit how many times the syntactic equality shortcut is allowed to fail (see [#5801](https://github.com/agda/agda/issues/5801)). If `FUEL` is omitted, then the syntactic equality shortcut is enabled without any restrictions. If `FUEL` is given, then the syntactic equality shortcut is given `FUEL` units of fuel. The exact meaning of this is implementation-dependent, but successful uses of the shortcut do not affect the amount of fuel. Currently the fuel is decreased in the failure continuations of the implementation of the syntactic equality shortcut. When a failure continuation completes the fuel is restored to its previous amount. The idea for this option comes from AndrΓ‘s KovΓ‘cs' [smalltt](https://github.com/AndrasKovacs/smalltt/blob/989b020309686e04374f1ab7844f468386d2eb2f/README.md#approximate-conversion-checking). Note that this option is experimental and subject to change. Library management ------------------ * Library files below the "project root" are now ignored (see [#5644](https://github.com/agda/agda/issues/5644)). For instance, if you have a module called `A.B.C` in the directory `Root/A/B`, then `.agda-lib` files in `Root/A` or `Root/A/B` do not affect what options are used to type-check `A.B.C`: `.agda-lib` files for `A.B.C` have to reside in `Root`, or further up the directory hierarchy. Interaction ----------- * β Agsy ([automatic proof search](https://agda.readthedocs.io/en/latest/tools/auto.html)) can now be invoked in the right-hand-sides of copattern matching clauses. ([#5827](https://github.com/agda/agda/pull/5827)) Compiler backends ----------------- * π₯ [**Breaking**] Both the GHC and JS backends now refuse to compile code that uses `--cubical`. Note that support for compiling code that uses `--erased-cubical` has been added to the GHC backend (see above). * If the GHC backend is invoked when `--interaction` or `--interaction-json` is active (for instance when the Emacs mode is used), then GHC is now invoked from the directory containing the `MAlonzo` directory (see [#6194](https://github.com/agda/agda/issues/6194)). Before GHC was invoked from the Agda process's current working directory, and that is still the case if `--interaction` and `--interaction-json` are not used. DOT backend ----------- * The new option `--dependency-graph-include=LIBRARY` can be used to restrict the dependency graph to modules from one or more libraries (see [#5634](https://github.com/agda/agda/issues/5634)). Note that the module given on the command line might not be included. * The generated graphs no longer contain "redundant" edges: if a module is imported both directly and indirectly, then the edge corresponding to the direct import is omitted. JSON API -------- * π₯ [**Breaking**] The JSON API now represents meta-variables differently, using objects containing two keys, `id` and `module`, both with values that are (natural) numbers. See [#5731](https://github.com/agda/agda/issues/5731). Other issues closed -------------------- π For 2.6.3, the following issues were also closed (see [bug tracker](https://github.com/agda/agda/issues)): - [#3986](https://github.com/agda/agda/issues/3986): Subtyping .A -> B <= A -> B leads to wrong ArgInfo - [#4103](https://github.com/agda/agda/issues/4103): Rewrite rule rejected because of projection likeness - [#4506](https://github.com/agda/agda/issues/4506): Lack of unicode support in locale may result in uncaught IOException - [#4725](https://github.com/agda/agda/issues/4725): Cubical Agda: Program rejected by termination checker due to moved dot pattern - [#4755](https://github.com/agda/agda/issues/4755): Rewrite rule on constructor uses wrong type for matching - [#4763](https://github.com/agda/agda/issues/4763): Cubical Agda: Unquote anonymous copattern involving path - [#5191](https://github.com/agda/agda/issues/5191): Unifier can use erased variables in non-erased data parameters - [#5257](https://github.com/agda/agda/issues/5257): Internal error when matching on user syntax with binding - [#5378](https://github.com/agda/agda/issues/5378): Internal error with tactic on record field - [#5448](https://github.com/agda/agda/issues/5448): Should the predicate be erasable in the subst rule (without-K) - [#5462](https://github.com/agda/agda/issues/5462): Internal error caused by a REWRITE on a projection-like function - [#5468](https://github.com/agda/agda/issues/5468): Disallow certain forms of pattern matching when an index is erased - [#5525](https://github.com/agda/agda/issues/5525): Duplicate entries in `executables` file lead to undefined behavior - [#5548](https://github.com/agda/agda/issues/5548): Agda infers an incorrect type with subtyping on - [#5551](https://github.com/agda/agda/issues/5551): Panic when showing module contents with pattern synonym - [#5563](https://github.com/agda/agda/issues/5563): Allow erased names in the type signatures of let-bound definitions - [#5577](https://github.com/agda/agda/issues/5577): The "Could not generate equivalence" warning is not always emitted - [#5581](https://github.com/agda/agda/issues/5581): Lexical error with tab character in literate Agda text - [#5589](https://github.com/agda/agda/issues/5589): Internal error with REWRITE of function from path - [#5681](https://github.com/agda/agda/issues/5681): Panic on record declaration with unknown sort - [#5702](https://github.com/agda/agda/issues/5702): Can't case split an `HitInt` with some already existing cases - [#5715](https://github.com/agda/agda/issues/5715): Reflection: Use `Telescope` for `getContext`, `inContext`, and `extendContext` - [#5727](https://github.com/agda/agda/issues/5727): Reducing universe levels before checking is not sufficient - [#5728](https://github.com/agda/agda/issues/5728): Internal error when pattern matching on `...` in with statement without providing a pattern match - [#5734](https://github.com/agda/agda/issues/5734): Relevance check in reflection - [#5751](https://github.com/agda/agda/issues/5751): json interaction produces Haskell output for SolveAll - [#5754](https://github.com/agda/agda/issues/5754): Internal error when compiling program with quoted metavariable - [#5760](https://github.com/agda/agda/issues/5760): Some code related to Cubical Agda runs also when the K rule is on - [#5763](https://github.com/agda/agda/issues/5763): Internal parser error using syntax rules - [#5765](https://github.com/agda/agda/issues/5765): Erasure check failure when pattern matching on refl in erased definition - [#5775](https://github.com/agda/agda/issues/5775): JSON interaction produces fully qualified terms - [#5794](https://github.com/agda/agda/issues/5794): Agsy/Auto crashes with `Prelude.!!: index too large` - [#5823](https://github.com/agda/agda/issues/5823): Singleton check loops on recursive eta record - [#5828](https://github.com/agda/agda/issues/5828): Agsy/Auto panics with `-r` in the presence of a pattern synonym - [#5845](https://github.com/agda/agda/issues/5845): Internal error caused by abstracting `variables` - [#5848](https://github.com/agda/agda/issues/5848): Internal error with `--confluence-check` - [#5850](https://github.com/agda/agda/issues/5850): Warn about useless hiding in `variable` declaration - [#5856](https://github.com/agda/agda/issues/5856): Lambda with irrefutable pattern is not rejected when used on Path - [#5868](https://github.com/agda/agda/issues/5868): Document --two-level - [#5875](https://github.com/agda/agda/issues/5875): Instance Search breaks Termination Highlighting - [#5891](https://github.com/agda/agda/issues/5891): SizeUniv : SizeUniv is inconsistent - [#5901](https://github.com/agda/agda/issues/5901): Use emacs --batch mode in agda-mode setup - [#5920](https://github.com/agda/agda/issues/5920): Erased constructors skipped in modality check - [#5922](https://github.com/agda/agda/issues/5922): Failure of termination checking for reflection-generated code due to data projections - [#5923](https://github.com/agda/agda/issues/5923): Internal error in rewriting - [#5944](https://github.com/agda/agda/issues/5944): Internal error in rewriting with --two-level - [#5953](https://github.com/agda/agda/issues/5953): Recursor of inductive-inductive type does not pass termination check in Cubical Agda - [#5955](https://github.com/agda/agda/issues/5955): Composition of Glue Type Causes Infinite Loop - [#5956](https://github.com/agda/agda/issues/5956): Cubical Agda crashes when printing empty system - [#5966](https://github.com/agda/agda/issues/5966): Improved performance by switching to `vector-hashtables` - [#5989](https://github.com/agda/agda/issues/5989): Dead-code elimination crashes function with private tactic argument - [#6003](https://github.com/agda/agda/issues/6003): de Bruijn index out of scope when rewriting - [#6006](https://github.com/agda/agda/issues/6006): Internal error rewriting with holes - [#6015](https://github.com/agda/agda/issues/6015): Pi types and Partial types should not be considered inter-convertible - [#6022](https://github.com/agda/agda/issues/6022): Private bindings in imported modules defeat check for binding of primIdFace/primIdPath - [#6042](https://github.com/agda/agda/issues/6042): De Bruijn index out of scope when rewriting without-K - [#6043](https://github.com/agda/agda/issues/6043): de Bruijn error on unexpected implicit argument - [#6059](https://github.com/agda/agda/issues/6059): Non-terminating function over tuples passed with `--termination-depth=2` - [#6066](https://github.com/agda/agda/issues/6066): Document the meaning of `pattern` without `no-eta-equality` - [#6067](https://github.com/agda/agda/issues/6067): Another de Bruijn error in rewriting - [#6073](https://github.com/agda/agda/issues/6073): Constraint solving does not honour singleton types - [#6074](https://github.com/agda/agda/issues/6074): piSort/funSort of IUniv should be blocked on the codomain - [#6076](https://github.com/agda/agda/issues/6076): Agda input mode (emacs): Minibuffer display for `\;` is strange - [#6080](https://github.com/agda/agda/issues/6080): A space leak due to absName - [#6082](https://github.com/agda/agda/issues/6082): Elaborate-and-give does not respect --postfix-projections - [#6095](https://github.com/agda/agda/issues/6095): Ambiguous pattern synonyms broken with anonymous module - [#6112](https://github.com/agda/agda/issues/6112): Internal error: non-confluent rewriting to singletons - [#6200](https://github.com/agda/agda/issues/6200): The reflection machinery does not treat the module telescope consistently - [#6203](https://github.com/agda/agda/issues/6203): Projection-likeness and instance arguments - [#6205](https://github.com/agda/agda/issues/6205): Internal error with `withReconstructed` - [#6244](https://github.com/agda/agda/issues/6244): Make `--no-load-primitives` not `--safe` - [#6250](https://github.com/agda/agda/issues/6250): Documentation says `--sized-types` is the default when it isn't - [#6257](https://github.com/agda/agda/issues/6257): Document options `--prop`, `--guarded`, and `--two-level`. - [#6265](https://github.com/agda/agda/issues/6265): Some options should be listed in `restartOptions` - [#6273](https://github.com/agda/agda/issues/6273): Missing highlighting when interleaved mutual is used - [#6276](https://github.com/agda/agda/issues/6276): LaTeX/HTML generation doesn't properly render parameters of pre-declared records - [#6281](https://github.com/agda/agda/issues/6281): Special treatment of attribute followed by underscore in pretty-printer - [#6285](https://github.com/agda/agda/issues/6285): Bump to GHC 9.4.3 - [#6337](https://github.com/agda/agda/issues/6337): --lossy-unification in Agda 2.6.3 - [#6338](https://github.com/agda/agda/issues/6338): internal error in Agda, perhaps related to --rewriting
-
v2.6.2 Changes
Installation and infrastructure
β Added support for GHC 8.10.4 and 9.0.1.
0οΈβ£ Some expensive optimisations are now off by default (see #4521).
These optimisations can in some cases make Agda substantially faster, but they can also make the compilation of the Agda program take more time and space.
The optimisations can be turned on manually (Cabal:
-foptimise-heavily
, Stack:--flag Agda:optimise-heavily
). They are turned on (by default) when Agda is installed usingmake install
.If the optimisations are turned on it might make sense to limit GHC's memory usage (using something like
--ghc-options="+RTS -M6G -RTS"
).Pragmas and options
- π New option
--auto-inline
turns on automatic compile-time inlining of simple functions. This was previously enabled by default.
Note that the absence of automatic inlining can make typechecking substantially slower.
The new default has repercussions on termination checking, for instance (see #4702). The following formulation of
plus
termination checks with--auto-inline
but not without:open import Agda.Builtin.Nat case_of_ : {A B : Set} β A β (A β B) β B case x of f = f x plus : Nat β Nat β Nat plus m n = case m of Ξ» { zero β n ; (suc m) β suc (plus m n) }
In this particular case, we can work around the limitation of the termination checker with pragma
{-# INLINE case_of_ #-}
.π New options
--qualified-instances
(default) and--no-qualified-instances
. When--no-qualified-instances
is enabled, Agda will only consider candidates for instance search that are in scope under an unqualified name (see #4522).π New option
--call-by-name
turns off call-by-need evaluation at type checking time.π New option
--highlight-occurrences
(off by default) enables the HTML backend to include a JavaScript file that highlights all occurrences of the mouse-hovered symbol (see #4535).π New option
--no-import-sorts
disables the implicitopen import Agda.Primitive using (Set; Prop)
at the top of each file (see below).π New option
--local-confluence-check
to restore the old behaviour of the--confluence-check
flag (see below for the new behaviour).π New primitive
primStringFromListInjective
internalising the fact thatprimStringFromList
is an injective function. It is bound inAgda.Builtin.String.Properties
.π New option
--allow-exec
enables the use of system calls during type checking using theAGDATCMEXECTC
builtin.π New option
--show-identity-substitutions
shows all arguments of metavariables when pretty-printing a term, even if they amount to just applying all the variables in the context.The option
--rewriting
is now considered infective: if a module has--rewriting
enabled, then all modules importing it must also have--rewriting
enabled.
Command-line interaction
- π In the previous release, Agda exited with either status 0 when the program type checks successfully, or status 1 when encountering any kind of error. Now Agda exits with status 42 for type errors, 71 for errors in the commandline arguments, and 154 for impossible errors. Exit status 1 may be returned under other circumstances; for instance, an incomplete pattern matching, or an error generated by the Haskell runtime. See PR #4540.
Language
- π Inductive records without Ξ·-equality no longer support both matching on the record constructor and construction of record elements by copattern matching. It has been discovered that the combination of both leads to loss of subject reduction, i.e., reduction does not preserve typing. See issue #4560.
Ξ·-equality for a record can be turned off manually with directive
no-eta-equality
or command-line option--no-eta-equality
, but it is also automatically turned off for some recursive records. For records without Ξ·, matching on the record constructor is now off by default and construction by copattern matching is on. If you want the converse, you can add the new record directivepattern
.Example with record pattern:
record N : Set where inductive no-eta-equality pattern field out : Maybe N pred : N β Maybe N pred record{ out = m } = m
Example with record constructor and use of
;
instead of newline:record N : Set where inductive; no-eta-equality pattern; constructor inn field out : Maybe N pred : N β Maybe N pred (inn m) = m
Set
andProp
are no longer keywords but are now primitives defined in the moduleAgda.Primitive
. They can be renamed when importing this module, for example:
open import Agda.Primitive renaming (Set to Type) test : Typeβ test = Type
To preserve backwards compatibility, each top-level Agda module now starts with an implicit statement:
open import Agda.Primitive using (Set; Prop)
This implicit import can be disabled with the
--no-import-sorts
flag.π Agda now has support for sorts
SetΟα΅’
(alternative syntax:SetΟi
) for natural numbersi
, whereSetΟβ = SetΟ
. These sorts form a second hierarchySetΟα΅’ : SetΟα΅’ββ
similar to the standard hierarchy ofSetα΅’
, but do not support universe polymorphism. It should not be necessary to refer to these sorts during normal usage of Agda, but they might be useful for defining reflection-based macros (see #2119 and #4585).π Changed the internal representation of literal strings: instead of using a linked list of characters (
String
), we are now usingData.Text
. This should be a transparent change from the user's point of view: the backend was already packing these strings as text.
Used this opportunity to introduce a
primStringUncons
primitive inAgda.Builtin.String
(and to correspondingly add theAgda.Builtin.Maybe
it needs).- The option
--confluence-check
for rewrite rules has been given a new implementation that checks global confluence instead of local confluence. Concretely, it does so by enforcing two properties:
For any two left-hand sides of the rewrite rules that overlap (either at the root position or at a subterm), the most general unifier of the two left-hand sides is again a left-hand side of a rewrite rule. For example, if there are two rules @suc m + n = suc (m + n)@ and @m + suc n = suc (m + n)@, then there should also be a rule @suc m + suc n = suc (suc (m + n))@.
Each rewrite rule should satisfy the triangle property: For any rewrite rule @u = w@ and any single-step parallel unfolding @u => v@, we should have another single-step parallel unfolding @v => w@.
The previous behaviour of the confluence checker that only ensures local confluence can be restored by using the
--local-confluence-check
flag.Binary integer literals with prefix
0b
(for instance,0b11001001
) are now supported.Overloaded literals now require the conversion function (fromNat, fromNeg, or fromString) to be in scope unqualified to take effect.
Previously, it was enough for the function to be in scope at all, which meant you couldn't import the corresponding builtin module without having overloaded literals turned on.
β Added
interleaved mutual
blocks where users can forward-declare function, record, and data types and interleave their definitions. These blocks are elaborated to more traditional mutual blocks by:- leaving the signatures where they are
- grouping the clauses for a function together with the first of them
- grouping the constructors for a datatype together with the first of them
Example: two interleaved function definitions
interleaved mutual -- Declarations: even : Nat β Bool odd : Nat β Bool -- zero is even, not odd even zero = true odd zero = false -- suc case: switch evenness on the predecessor even (suc n) = odd n odd (suc n) = even n
Other example: the definition of universe of types closed under the natural numbers and pairing:
interleaved mutual -- Declaration of a product record, a universe of codes, and a decoding function record _Γ_ (A B : Set) : Set data U : Set El : U β Set -- We have a code for the type of natural numbers in our universe constructor `Nat : U El `Nat = Nat -- Btw we know how to pair values in a record record _Γ_ A B where constructor _,_ inductive field fst : A; snd : B -- And we have a code for pairs in our universe constructor _`Γ_ : (A B : U) β U El (A `Γ B) = El A Γ El B
- π Erased constructors (see #4638).
Constructors can be marked as erased. Example:
{-# OPTIONS --cubical --safe #-} open import Agda.Builtin.Cubical.Path open import Agda.Primitive private variable a : Level A B : Set a Is-proposition : Set a β Set a Is-proposition A = (x y : A) β x β‘ y data β₯_β₯ (A : Set a) : Set a where β£_β£ : A β β₯ A β₯ @0 trivial : Is-proposition β₯ A β₯ rec : @0 Is-proposition B β (A β B) β β₯ A β₯ β B rec p f β£ x β£ = f x rec p f (trivial x y i) = p (rec p f x) (rec p f y) i
In the code above the constructor
trivial
is only available at compile-time, whereasβ£_β£
is also available at run-time. Erased names can be used in bodies of clauses that match ontrivial
, like the final clause ofrec
. (Note that Cubical Agda programs still cannot be compiled.)The following code is also accepted:
{-# OPTIONS --without-K --safe #-} open import Agda.Builtin.Bool data D : Set where run-time : Bool β D @0 compile-time : Bool β D f : @0 D β D f (compile-time x) = compile-time x f (run-time _) = run-time true
Agda allows matching on an erased argument if there is only one valid run-time case. (If the K rule is turned off, then the data type must also be non-indexed.) When
f
is compiled the clause that matches oncompile-time
is omitted.- π New (?) rule for modalities of generalised variables (see #5058).
The new rule is that generalisable variables get the modality that they are declared with, whereas other variables always get the default modality. (It is unclear what the old rule was, perhaps nothing was changed.)
- π Private abstract type signatures can no longer see through abstract (see #418).
This means that abstract definitions no longer evaluate in any type signatures in the same module. Previously they evaluated in type signatures of definitions that were both private and abstract.
It also means that metavariables in type signatures have to be solved locally, and cannot make use of information in the definition body, and that constructors of abstract datatypes are not in scope in type signatures.
- π Type inference is disabled for abstract definitions (see #418).
This means that abstract definitions (inluding functions defined in
where
blocks of abstract definitions) need complete type signatures.- One can now declare syntax with two name parts without any hole in between, and syntax without any holes.
Examples:
syntax Ξ£ A (Ξ» x β B) = [ x βΆ A ] Γ B syntax [] = [ ]
- Internalised the inspect idiom that allows users to abstract over an
expression in a
with
clause while, at the same time, remembering the origin of the abstracted pattern via an equation.
In the following example, abstracting over and then matching on the result of
p x
allows the first call tofilter p (x β· xs)
to reduce.In case the element
x
is kept, the second call tofilter
on the LHS then performs the samep x
test. Because we have retained the proof thatp x β‘ true
ineq
, we are able to rewrite by this equality and get it to reduce too.This leads to just enough computation that we can finish the proof with an appeal to congruence and the induction hypothesis.
filter-filter : β p xs β filter p (filter p xs) β‘ filter p xs filter-filter p [] = refl filter-filter p (x β· xs) with p x in eq ... | false = filter-filter p xs -- easy ... | true -- second filter stuck on `p x`: rewrite by `eq`! rewrite eq = cong (x β·_) (filter-filter p xs)
Builtins
- Primitive operations for floating-point numbers changed. The equalities now
follow IEEE 754 equality, after unifying all NaNs. Primitive inequality was
added:
agda primFloatEquality : Float -> Float -> Bool -- from primFloatNumericEquality primFloatLess : Float -> Float -> Bool -- from primFloatNumericLess primFloatInequality : Float -> Float -> Bool -- new
The βnumericβ relations are now deprecated.
There are several new predicates on floating-point numbers:
primFloatIsInfinite : Float -> Bool -- new primFloatIsNaN : Float -> Bool -- new primFloatIsSafeInteger : Float -> Bool -- new
The primFloatIsSafeInteger function determines whether the value is a number that is a safe integer, i.e., is within the range where the arithmetic operations do not lose precision.
The operations for conversion to integers (primRound, primFloor, and primCeiling) were renamed for consistency, and return a value of type
Maybe Int
, returningnothing
for NaN and the infinities:primFloatRound : Float β Maybe Int -- from primRound primFloatFloor : Float β Maybe Int -- from primFloor primFloatCeiling : Float β Maybe Int -- from primCeiling
There are several new conversions:
primIntToFloat : Int -> Float -- new primFloatToRatio : Float -> (Int Γ Nat) -- new primRatioToFloat : Int -> Nat -> Float -- new primFloatDecode : Float -> Maybe (Int Γ Int) -- new primFloatEncode : Int -> Int -> Maybe Float -- new
The
primFloatDecode
function decodes a floating-point number f to a mantissa and exponent, such thatf = mantissa * 2 ^ exponent
, normalised such that the mantissa is the smallest possible number. TheprimFloatEncode
function encodes a pair of a mantissa and exponent to a floating-point number.There are several new operations:
primFloatPow : Float -> Float -> Float -- new primFloatATan2 : Float -> Float -> Float -- from primATan2 primFloatSinh : Float -> Float -- new primFloatCosh : Float -> Float -- new primFloatTanh : Float -> Float -- new primFloatASinh : Float -> Float -- new primFloatACosh : Float -> Float -- new primFloatATanh : Float -> Float -- new
Furthermore, the following operations were renamed for consistency:
primFloatExp : Float -> Float -- from primExp primFloatSin : Float -> Float -- from primSin primFloatLog : Float -> Float -- from primLog primFloatCos : Float -> Float -- from primCos primFloatTan : Float -> Float -- from primTan primFloatASin : Float -> Float -- from primASin primFloatACos : Float -> Float -- from primACos primFloatATan : Float -> Float -- from primATan
All of these operations are implemented on the JavaScript backend.
primNatToChar
maps surrogate code points to the replacement character'U+FFFD
and surrogate code points are disallowed in character literals
Surrogate code points are characters in the range
U+D800
toU+DFFF
and are reserved for use by UTF-16.The reason for this change is that strings are represented (at type-checking time and in the GHC backend) by Data.Text byte strings, which cannot represent surrogate code points and replaces them by
U+FFFD
. By doing the same for characters we can haveprimStringFromList
be injective (witnessed byAgda.Builtin.String.Properties.primStringFromListInjective
).Reflection
- π New operation in
TC
monad, similar toquoteTC
but operating on types inSetΟ
agda quoteΟTC : β {A : SetΟ} β A β TC Term
π¨
typeError
anddebugPrint
no longer inserts spaces aroundtermErr
andnameErr
parts. They also do a better job of respecting line breaks instrErr
parts.The representation of reflected patterns and clauses has changed. Each clause now includes a telescope with the names and types of the pattern variables.
data Clause where clause : (tel : List (Ξ£ String Ξ» _ β Arg Type)) (ps : List (Arg Pattern)) (t : Term) β Clause absurd-clause : (tel : List (Ξ£ String Ξ» _ β Arg Type)) (ps : List (Arg Pattern)) β Clause
These telescopes provide additional information on the types of pattern variables that was previously hard to reconstruct (see #2151). When unquoting a clause, the types in the clause telescope are currently ignored (but this is subject to change in the future).
Three constructors of the
Pattern
datatype were also changed:- pattern variables now refer to a de Bruijn index (relative to the clause telescope) rather than a string,
- absurd patterns take a de Bruijn index and are expected to be bound by the clause telescope,
- dot patterns now include the actual dotted term.
data Pattern where con : (c : Name) (ps : List (Arg Pattern)) β Pattern dot : (t : Term) β Pattern -- previously: dot : Pattern var : (x : Nat) β Pattern -- previously: var : (x : String) β Pattern lit : (l : Literal) β Pattern proj : (f : Name) β Pattern absurd : (x : Nat) β Pattern
It is likely that this change to the reflected syntax requires you to update reflection code written for previous versions of Agda. Here are some tips for updating your code:
When quoting a clause, you can recover the name of a pattern variable by looking up the given index in the clause telescope. The contents of dot patterns can safely be ignored (unless you have a use for them).
When creating a new clause for unquoting, you need to create a telescope for the types of the pattern variables. To get back the old behaviour of Agda, it is sufficient to set all the types of the pattern variables to
unknown
. So you can construct the telescope by listing the names of all pattern variables and absurd patterns together with theirArgInfo
. Meanwhile, the pattern variables should be numbered in order to update them to the new representation. As for the telescope types, the contents of adot
pattern can safely be set tounknown
.- π New operation in
TC
monad,execTC
, which calls an external executableagda execTC : (exe : String) (args : List String) (stdIn : String) β TC (Ξ£ Nat (Ξ» _ β Ξ£ String (Ξ» _ β String)))
TheexecTC
builtin takes three arguments: the basename of the executable (e.g.,"echo"
), aΒ list of arguments, and the contents of the standard input. It returns a triple, consisting of the exit code (as a natural number), the contents of the standard output, and the contents of the standard error.
- π New operation in
The builtin is only available when
--allow-exec
is passed. (Note that--allow-exec
is incompatible with--safe
.) To make an executable available to Agda, add the absolute path on a new line in~/.agda/executables
.- Two new operations in the
TC
monad,onlyReduceDefs
anddontReduceDefs
:agda onlyReduceDefs : β {a} {A : Set a} β List Name β TC A β TC A dontReduceDefs : β {a} {A : Set a} β List Name β TC A β TC A
These functions allow picking a specific set of functions that should (resp. should not) be reduced while executing the givenTC
computation.
For example, the following macro unifies the current hole with the term
3 - 3
:macroβ : Term -> TC β€ macroβ goal = do u β quoteTC ((1 + 2) - 3) u' β onlyReduceDefs (quote _+_ β· []) (normalise u) unify u' goal
- π New operation in the
TC
monad,withReconstructed
:agda withReconstructed : β {a} {A : Set a} β TC A β TC A
This function ensures reconstruction of hidden parameters after performing the
TC
computation. For example, consider the following type and function:record RVec {a} (X : Set a) (n : Nat) : Set a where constructor vec field sel : Fin n β X test-rvec : Nat β RVec Nat 5 test-rvec x = vec Ξ» _ β x
In the reflected syntax the body of the
test-rvec
would be represented ascon vec (unknown β· unknown β· unknown β· (lam _ x)
. The use ofwithReconstructed
replacesunknown
s with the actual values:macroβ : Name β Term β TC β€ macroβ n hole = do (function (clause tel ps t β· [])) β withReconstructed (getDefinition n) where _ β quoteTC "ERROR" >>= unify hole quoteTC t >>= unify hole
Three new constructors in the
Sort
datatype,prop : Level β Sort
,propLit : Nat β Sort
, andinf : Nat β Sort
, representing the sortsProp β
,Propα΅’
, andSetΟα΅’
.Terms that belong to a type in
Prop
are no longer unquoted tounknown
but to a properTerm
. (See #3553.)
Library management
.agda-lib
files can now contain an extra fieldflags:
with default flags for the library. Flags can be any flags that are accepted as part of an{-# OPTIONS ... #-}
pragma. For example, filemy-library.agda-lib
with
flags: --without-K
will apply the
--without-K
flag to all Agda files in the current directory and (recursive) subdirectories that do not themselves contain an.agda-lib
file.Emacs mode
- π New command prefix
C-u C-u C-u
for weak-head normalization. For instance, given
downFrom : Nat β List Nat downFrom 0 = [] downFrom (suc n) = n β· downFrom n
C-u C-u C-u C-c C-n downFrom 5
returns4 β· downFrom 4
.π New keyboard shortcut
C-c C-x C-i
for toggling display of irrelevant arguments.One can no longer use commands like
M-;
(comment-dwim
) to uncomment block comments. In return one can useM-;
to comment out pragmas. (See #3329.)
JSON Interaction mode
π Changes have been made to the structure of error and warning messages. The π changes are summarized below. See #5052 for additional details.
- β The format of an error or warning was previously a bare string. Now, errors
and warnings are represented by an object with a
"message"
key.
This means that responses previously structured like:
{"β¦": "β¦", "error": "Foo bar baz"}
will now be structured:
{"β¦": "β¦", "error": {"message": "Foo bar baz"}}
This applies directly to the
PostPonedCheckFunDef
response kind andError
info kind of theDisplayInfo
response kind.- β The format of collections of errors or warnings, which previously were each represented by a single newline-joined string, has been updated to represent each warning or error individually in a list.
That means that responses previously structured like:
{ "β¦": "β¦" , "errors": "Postulates overcooked\nAxioms too wiggly" , "warnings": "Something wrong\nSomething else\nwrong" }
will now be structured:
{ "β¦": "β¦" , "errors": [ { "message": "Postulates overcooked" } , { "message": "Axioms too wiggly" } ] , "warnings": [ { "message": "Something wrong" } , { "message": "Something else\nwrong" } ] }
This applies to
CompilationOk
,AllGoalsWarning
, andError
info kinds of theDisplayInfo
response kind.- The
Error
info kind of theDisplayInfo
response kind has additionally been updated to distinguish warnings and errors.
An example of the previous format of a
DispayInfo
response with anError
info kind was:{ "kind": "DisplayInfo", "info": { "kind": "Error", "message": "ββββ Error βββββββββββββββββββββββββββββββββββββββββββββββββ\n/data/code/agda-test/Test.agda:2,1-9\nFailed to find source of module M in any of the following\nlocations:\n /data/code/agda-test/M.agda\n /data/code/agda-test/M.lagda\nwhen scope checking the declaration\n import M\n\nββββ Warning(s) ββββββββββββββββββββββββββββββββββββββββββββ\n/data/code/agda-test/Test.agda:3,1-10\nEmpty postulate block." } }
The updated format is:
{ "kind": "DisplayInfo", "info": { "kind": "Error", "error": { "message": "/data/code/agda-test/Test.agda:2,1-9\nFailed to find source of module M in any of the following\nlocations:\n /data/code/agda-test/M.agda\n /data/code/agda-test/M.lagda\nwhen scope checking the declaration\n import M" }, "warnings": [ { "message": "/data/code/agda-test/Test.agda:3,1-10\nEmpty postulate block." } ] } }
Compiler backends
With option
--allow-unsolved-metas
, code with holes can be compiled. If a hole is reached at runtime, the compiled program crashes. See issue #5103Previously the GHC backend compiled at least one instance of Hinze's memoisation technique from "Memo functions, polytypically!" to reasonably efficient code. That is no longer the case (at least for that particular instance, see #5153).
JS backend
- Smaller local variable names in the generated JS code.
Previously:
x0
,x1
,x2
, ...Now:
a
,b
,c
, ...,z
,a0
,b0
, ...,z0
,a1
,b1
, ...π Improved indentation of generated JS code.
More compact rendering of generated JS functions.
Previously:
exports["N"]["suc"] = function (x0) { return function (x1) { return x1["suc"](x0); }; };
Now:
exports["N"]["suc"] = a => b => b["suc"](a);
- Irrelevant arguments are now erased in the generated JS code.
Example Agda code:
flip : {A B C : Set} -> (B -> A -> C) -> A -> B -> C flip f a b = f b a
Previously generated JS code:
exports["flip"] = function (x0) { return function (x1) { return function (x2) { return function (x3) { return function (x4) { return function (x5) { return x3(x5)(x4); }; }; }; }; }; };
JS code generated now:
exports["flip"] = a => b => c => a(c)(b);
- Record fields are not stored separately (the fields are stored only in the constructor) in the generated JS code.
Example Agda code:
record Sigma (A : Set) (B : A -> Set) : Set where field fst : A snd : B fst
Previously generated JS code (look at the
"fst"
and"snd"
fields in the return value ofexports["Sigma"]["record"]
:exports["Sigma"] = {}; exports["Sigma"]["fst"] = function (x0) { return x0["record"]({ "record": function (x1, x2) { return x1; } }); }; exports["Sigma"]["snd"] = function (x0) { return x0["record"]({ "record": function (x1, x2) { return x2; } }); }; exports["Sigma"]["record"] = function (x0) { return function (x1) { return { "fst": x0, "record": function (x2) { return x2["record"](x0, x1); }, "snd": x1 }; }; };
JS code generated now:
exports["Sigma"] = {}; exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b}); exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c}); exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});
- β‘οΈ
--js-optimize
flag has been added to theagda
compiler.
With
--js-optimize
,agda
does not wrap records in JS objects.Example Agda code:
record Sigma (A : Set) (B : A -> Set) : Set where field fst : A snd : B fst
JS code generated without the
--js-optimize
flag:exports["Sigma"] = {}; exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b}); exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c}); exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});
JS code generated with the
--js-optimize
flag:exports["Sigma"] = {}; exports["Sigma"]["fst"] = a => a((b,c) => b); exports["Sigma"]["snd"] = a => a((b,c) => c); exports["Sigma"]["record"] = a => b => c => c(a,b);
With
--js-optimize
,agda
uses JS arrays instead of JS objects. This is possible because constructor names are not relevant during the evaluation.Example Agda code:
data Bool : Set where false : Bool true : Bool not : Bool -> Bool not false = true not true = false
JS code generated without the
--js-optimize
flag:exports["Bool"] = {}; exports["Bool"]["false"] = a => a["false"](); exports["Bool"]["true"] = a => a["true"](); exports["not"] = a => a({ "false": () => exports["Bool"]["true"], "true": () => exports["Bool"]["false"] });
JS code generated with the
--js-optimize
flag:exports["Bool"] = {}; exports["Bool"]["false"] = a => a[0/* false */](); exports["Bool"]["true"] = a => a[1/* true */](); exports["not"] = a => a([ /* false */() => exports["Bool"]["true"], /* true */() => exports["Bool"]["false"] ]);
Note that comments are added to generated JS code to help human readers.
Erased branches are replaced by
null
in the generated array. If more than the half of branches are erased, the array is compressed to be a object like{3: ..., 13: ...}
.--js-minify
flag has been added to theagda
compiler.
With
--js-minify
,agda
discards comments and whitespace in the generated JS code.Agda as a library (API)
- π The
SourceInfo
record has been renamed toSource
, and thesourceInfo
function toparseSource
.