-
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 implicit open 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 that
primStringFromList is an injective function. It is bound in
Agda.Builtin.String.Properties.
-
New option --allow-exec enables the use of system calls during
type checking using the AGDATCMEXECTC 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.
-
New option --no-double-check (default), opposite of the existing
--double-check.
-
Due to several known soundness issues with sized types (see
#1201,
#1946,
#2820,
#3026), the
--sized-types flag can no longer be used while --safe is active.
-
New option --guarded turns on the Guarded Cubical extension of Agda.
See Guarded Cubical
in the documentation for more.
-
The flags --guardedness and --sized-types are no longer enabled
by default.
-
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 directive pattern.
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 and Prop are no longer keywords but are now primitives
defined in the module Agda.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 numbers i, where Setω₀ = Setω. These sorts form a
second hierarchy Setωᵢ : Setωᵢ₊₁ similar to the standard hierarchy
of Setᵢ, 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 using Data.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 in
Agda.Builtin.String (and to correspondingly add the
Agda.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 on trivial, if
the match is done in a non-erased position, like in the final clause
of rec. (Note that Cubical Agda programs still cannot be
compiled.)
-
Erased pattern-matching lambdas (see
#4525).
Regular pattern-matching lambdas are treated as non-erased
function definitions. One can make a pattern-matching lambda erased
by writing @0 or @erased after the lambda:
@0 _ : @0 Set → Set
_ = λ @0 { A → A }
@0 _ : @0 Set → Set
_ = λ @erased where
A → A
The reflection machinery currently does not support erased
pattern-matching lambdas (they are quoted as regular
pattern-matching lambdas).
-
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 to filter p (x ∷ xs) to
reduce.
In case the element x is kept, the second call to filter on
the LHS then performs the same p x test. Because we have
retained the proof that p x ≡ true in eq, 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)
-
As a consequence of the above extensions to with, lambdas and lets
now need parentheses when appearing in a with. For instance,
with-on-fun : Nat → Nat
with-on-fun n with (λ m → m + n) -- parentheses required!
... | f = f n
-
It is now possible to add hiding and relevance annotations to with
expressions. For example:
module _ (A B : Set) (recompute : .B → .{{A}} → B) where
_$_ : .(A → B) → .A → B
f $ x with .{f} | .(f x) | .{{x}}
... | y = recompute y
-
Primitive operations for floating-point numbers changed. The equalities now
follow IEEE 754 equality, after unifying all NaNs. Primitive inequality was
added:
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, returning nothing 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 that f = mantissa * 2 ^ exponent, normalised such that
the mantissa is the smallest possible number. The primFloatEncode 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 to U+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 have primStringFromList be injective (witnessed
by Agda.Builtin.String.Properties.primStringFromListInjective).
-
New operation in TC monad, similar to quoteTC but operating on
types in Setω
quoteωTC : ∀ {A : Setω} → A → TC Term
-
typeError and debugPrint no longer inserts spaces around termErr and
nameErr parts. They also do a better job of respecting line breaks in
strErr parts.
-
The reflection machinery now supports quantities in Arg (see
#5317). The ArgInfo
type has changed, and there are new types Modality and Quantity:
data Quantity : Set where
quantity-0 quantity-ω : Quantity
{-# BUILTIN QUANTITY Quantity #-}
{-# BUILTIN QUANTITY-0 quantity-0 #-}
{-# BUILTIN QUANTITY-ω quantity-ω #-}
data Modality : Set where
modality : (r : Relevance) (q : Quantity) → Modality
{-# BUILTIN MODALITY Modality #-}
{-# BUILTIN MODALITY-CONSTRUCTOR modality #-}
data ArgInfo : Set where
arg-info : (v : Visibility) (m : Modality) → ArgInfo
-
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 their ArgInfo. Meanwhile, the pattern
variables should be numbered in order to update them to the new
representation. As for the telescope types, the contents of a
dot pattern can safely be set to unknown.
-
New operation in TC monad, execTC, which calls an external executable
execTC : (exe : String) (args : List String) (stdIn : String)
→ TC (Σ Nat (λ _ → Σ String (λ _ → String)))
The execTC 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.
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 and
dontReduceDefs:
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 given TC
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:
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
as con vec (unknown ∷ unknown ∷ unknown ∷ (lam _ x). The use of
withReconstructed replaces unknowns 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, and inf : Nat → Sort, representing
the sorts Prop ℓ, Propᵢ, and Setωᵢ.
-
Terms that belong to a type in Prop are no longer unquoted to
unknown but to a proper Term. (See
#3553.)
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
and Error info kind of the DisplayInfo 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, and Error info
kinds of the DisplayInfo response kind.
-
The Error info kind of the DisplayInfo response kind has
additionally been updated to distinguish warnings and errors.
An example of the previous format of a DisplayInfo response with
an Error 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."
}
]
}
}
-
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 of exports["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 the agda 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 the agda compiler.
With --js-minify, agda discards comments and whitespace in the
generated JS code.
