Agda-2.6.4: doc/release-notes/2.2.8.md
Release notes for Agda 2 version 2.2.8
======================================
Language
--------
* Record pattern matching.
It is now possible to pattern match on named record constructors.
Example:
```agda
record Σ (A : Set) (B : A → Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁
map : {A B : Set} {P : A → Set} {Q : B → Set}
(f : A → B) → (∀ {x} → P x → Q (f x)) →
Σ A P → Σ B Q
map f g (x , y) = (f x , g y)
```
The clause above is internally translated into the following one:
```agda
map f g p = (f (Σ.proj₁ p) , g (Σ.proj₂ p))
```
Record patterns containing data type patterns are not translated.
Example:
```agda
add : ℕ × ℕ → ℕ
add (zero , n) = n
add (suc m , n) = suc (add (m , n))
```
Record patterns which do not contain data type patterns, but which
do contain dot patterns, are currently rejected. Example:
```agda
Foo : {A : Set} (p₁ p₂ : A × A) → proj₁ p₁ ≡ proj₁ p₂ → Set₁
Foo (x , y) (.x , y′) refl = Set
```
* Proof irrelevant function types.
Agda now supports irrelevant non-dependent function types:
```agda
f : .A → B
```
This type implies that `f` does not depend computationally on its
argument. One intended use case is data structures with embedded
proofs, like sorted lists:
```agda
postulate
_≤_ : ℕ → ℕ → Set
p₁ : 0 ≤ 1
p₂ : 0 ≤ 1
data SList (bound : ℕ) : Set where
[] : SList bound
scons : (head : ℕ) →
.(head ≤ bound) →
(tail : SList head) →
SList bound
```
The effect of the irrelevant type in the signature of `scons` is
that `scons`'s second argument is never inspected after Agda has
ensured that it has the right type. It is even thrown away, leading
to smaller term sizes and hopefully some gain in efficiency. The
type-checker ignores irrelevant arguments when checking equality, so
two lists can be equal even if they contain different proofs:
```agda
l₁ : SList 1
l₁ = scons 0 p₁ []
l₂ : SList 1
l₂ = scons 0 p₂ []
l₁≡l₂ : l₁ ≡ l₂
l₁≡l₂ = refl
```
Irrelevant arguments can only be used in irrelevant contexts.
Consider the following subset type:
```agda
data Subset (A : Set) (P : A → Set) : Set where
_#_ : (elem : A) → .(P elem) → Subset A P
```
The following two uses are fine:
```agda
elimSubset : ∀ {A C : Set} {P} →
Subset A P → ((a : A) → .(P a) → C) → C
elimSubset (a # p) k = k a p
elem : {A : Set} {P : A → Set} → Subset A P → A
elem (x # p) = x
```
However, if we try to project out the proof component, then Agda
complains that `variable p is declared irrelevant, so it cannot be
used here`:
```agda
prjProof : ∀ {A P} (x : Subset A P) → P (elem x)
prjProof (a # p) = p
```
Matching against irrelevant arguments is also forbidden, except in
the case of irrefutable matches (record constructor patterns which
have been translated away). For instance, the match against the
pattern `(p , q)` here is accepted:
```agda
elim₂ : ∀ {A C : Set} {P Q : A → Set} →
Subset A (λ x → Σ (P x) (λ _ → Q x)) →
((a : A) → .(P a) → .(Q a) → C) → C
elim₂ (a # (p , q)) k = k a p q
```
Absurd matches `()` are also allowed.
Note that record fields can also be irrelevant. Example:
```agda
record Subset (A : Set) (P : A → Set) : Set where
constructor _#_
field
elem : A
.proof : P elem
```
Irrelevant fields are never in scope, neither inside nor outside the
record. This means that no record field can depend on an irrelevant
field, and furthermore projections are not defined for such fields.
Irrelevant fields can only be accessed using pattern matching, as in
`elimSubset` above.
Irrelevant function types were added very recently, and have not
been subjected to much experimentation yet, so do not be surprised
if something is changed before the next release. For instance,
dependent irrelevant function spaces (`.(x : A) → B`) might be added
in the future.
* Mixfix binders.
It is now possible to declare user-defined syntax that binds
identifiers. Example:
```agda
postulate
State : Set → Set → Set
put : ∀ {S} → S → State S ⊤
get : ∀ {S} → State S S
return : ∀ {A S} → A → State S A
bind : ∀ {A B S} → State S B → (B → State S A) → State S A
syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂
increment : State ℕ ⊤
increment = x ← get ,
put (1 + x)
```
The syntax declaration for `bind` implies that `x` is in scope in
`e₂`, but not in `e₁`.
You can give fixity declarations along with syntax declarations:
```agda
infixr 40 bind
syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂
```
The fixity applies to the syntax, not the name; syntax declarations
are also restricted to ordinary, non-operator names. The following
declaration is disallowed:
```agda
syntax _==_ x y = x === y
```agda
Syntax declarations must also be linear; the following declaration
is disallowed:
```agda
syntax wrong x = x + x
```
Syntax declarations were added very recently, and have not been
subjected to much experimentation yet, so do not be surprised if
something is changed before the next release.
* `Prop` has been removed from the language.
The experimental sort `Prop` has been disabled. Any program using
`Prop` should typecheck if `Prop` is replaced by `Set₀`. Note that
`Prop` is still a keyword.
* Injective type constructors off by default.
Automatic injectivity of type constructors has been disabled (by
default). To enable it, use the flag
`--injective-type-constructors`, either on the command line or in an
`OPTIONS` pragma. Note that this flag makes Agda anti-classical and
possibly inconsistent:
Agda with excluded middle is inconsistent
http://thread.gmane.org/gmane.comp.lang.agda/1367
See `test/Succeed/InjectiveTypeConstructors.agda` for an example.
* Termination checker can count.
There is a new flag `--termination-depth=N` accepting values `N >=
1` (with `N = 1` being the default) which influences the behavior of
the termination checker. So far, the termination checker has only
distinguished three cases when comparing the argument of a recursive
call with the formal parameter of the callee.
`<`: the argument is structurally smaller than the parameter
`=`: they are equal
`?`: the argument is bigger or unrelated to the parameter
This behavior, which is still the default (`N = 1`), will not
recognise the following functions as terminating.
```agda
mutual
f : ℕ → ℕ
f zero = zero
f (suc zero) = zero
f (suc (suc n)) = aux n
aux : ℕ → ℕ
aux m = f (suc m)
```
The call graph
```
f --(<)--> aux --(?)--> f
```
yields a recursive call from `f` to `f` via `aux` where the relation
of call argument to callee parameter is computed as "unrelated"
(composition of `<` and `?`).
Setting `N >= 2` allows a finer analysis: `n` has two constructors
less than `suc (suc n)`, and `suc m` has one more than `m`, so we get the
call graph:
```
f --(-2)--> aux --(+1)--> f
```
The indirect call `f --> f` is now labeled with `(-1)`, and the
termination checker can recognise that the call argument is
decreasing on this path.
Setting the termination depth to `N` means that the termination
checker counts decrease up to `N` and increase up to `N-1`. The
default, `N=1`, means that no increase is counted, every increase
turns to "unrelated".
In practice, examples like the one above sometimes arise when `with`
is used. As an example, the program
```agda
f : ℕ → ℕ
f zero = zero
f (suc zero) = zero
f (suc (suc n)) with zero
... | _ = f (suc n)
```
is internally represented as
```agda
mutual
f : ℕ → ℕ
f zero = zero
f (suc zero) = zero
f (suc (suc n)) = aux n zero
aux : ℕ → ℕ → ℕ
aux m k = f (suc m)
```
Thus, by default, the definition of `f` using `with` is not accepted
by the termination checker, even though it looks structural (`suc n`
is a subterm of `suc suc n`). Now, the termination checker is
satisfied if the option `--termination-depth=2` is used.
Caveats:
- This is an experimental feature, hopefully being replaced by
something smarter in the near future.
- Increasing the termination depth will quickly lead to very long
termination checking times. So, use with care. Setting termination
depth to `100` by habit, just to be on the safe side, is not a good
idea!
- Increasing termination depth only makes sense for linear data
types such as `ℕ` and `Size`. For other types, increase cannot be
recognised. For instance, consider a similar example with lists.
```agda
data List : Set where
nil : List
cons : ℕ → List → List
mutual
f : List → List
f nil = nil
f (cons x nil) = nil
f (cons x (cons y ys)) = aux y ys
aux : ℕ → List → List
aux z zs = f (cons z zs)
```
Here the termination checker compares `cons z zs` to `z` and also
to `zs`. In both cases, the result will be "unrelated", no matter
how high we set the termination depth. This is because when
comparing `cons z zs` to `zs`, for instance, `z` is unrelated to
`zs`, thus, `cons z zs` is also unrelated to `zs`. We cannot say
it is just "one larger" since `z` could be a very large term. Note
that this points to a weakness of untyped termination checking.
To regain the benefit of increased termination depth, we need to
index our lists by a linear type such as `ℕ` or `Size`. With
termination depth `2`, the above example is accepted for vectors
instead of lists.
* The `codata` keyword has been removed. To use coinduction, use the
following new builtins: `INFINITY`, `SHARP` and `FLAT`. Example:
```agda
{-# OPTIONS --universe-polymorphism #-}
module Coinduction where
open import Level
infix 1000 ♯_
postulate
∞ : ∀ {a} (A : Set a) → Set a
♯_ : ∀ {a} {A : Set a} → A → ∞ A
♭ : ∀ {a} {A : Set a} → ∞ A → A
{-# BUILTIN INFINITY ∞ #-}
{-# BUILTIN SHARP ♯_ #-}
{-# BUILTIN FLAT ♭ #-}
```
Note that (non-dependent) pattern matching on `SHARP` is no longer
allowed.
Note also that strange things might happen if you try to combine the
pragmas above with `COMPILED_TYPE`, `COMPILED_DATA` or `COMPILED`
pragmas, or if the pragmas do not occur right after the postulates.
The compiler compiles the `INFINITY` builtin to nothing (more or
less), so that the use of coinduction does not get in the way of FFI
declarations:
```agda
data Colist (A : Set) : Set where
[] : Colist A
_∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A
{-# COMPILED_DATA Colist [] [] (:) #-}
```
* Infinite types.
If the new flag `--guardedness-preserving-type-constructors` is
used, then type constructors are treated as inductive constructors
when we check productivity (but only in parameters, and only if they
are used strictly positively or not at all). This makes examples
such as the following possible:
```agda
data Rec (A : ∞ Set) : Set where
fold : ♭ A → Rec A
-- Σ cannot be a record type below.
data Σ (A : Set) (B : A → Set) : Set where
_,_ : (x : A) → B x → Σ A B
syntax Σ A (λ x → B) = Σ[ x ∶ A ] B
-- Corecursive definition of the W-type.
W : (A : Set) → (A → Set) → Set
W A B = Rec (♯ (Σ[ x ∶ A ] (B x → W A B)))
syntax W A (λ x → B) = W[ x ∶ A ] B
sup : {A : Set} {B : A → Set} (x : A) (f : B x → W A B) → W A B
sup x f = fold (x , f)
W-rec : {A : Set} {B : A → Set}
(P : W A B → Set) →
(∀ {x} {f : B x → W A B} → (∀ y → P (f y)) → P (sup x f)) →
∀ x → P x
W-rec P h (fold (x , f)) = h (λ y → W-rec P h (f y))
-- Induction-recursion encoded as corecursion-recursion.
data Label : Set where
′0 ′1 ′2 ′σ ′π ′w : Label
mutual
U : Set
U = Σ Label U′
U′ : Label → Set
U′ ′0 = ⊤
U′ ′1 = ⊤
U′ ′2 = ⊤
U′ ′σ = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
U′ ′π = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
U′ ′w = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
El : U → Set
El (′0 , _) = ⊥
El (′1 , _) = ⊤
El (′2 , _) = Bool
El (′σ , fold (a , b)) = Σ[ x ∶ El a ] El (b x)
El (′π , fold (a , b)) = (x : El a) → El (b x)
El (′w , fold (a , b)) = W[ x ∶ El a ] El (b x)
U-rec : (P : ∀ u → El u → Set) →
P (′1 , _) tt →
P (′2 , _) true →
P (′2 , _) false →
(∀ {a b x y} →
P a x → P (b x) y → P (′σ , fold (a , b)) (x , y)) →
(∀ {a b f} →
(∀ x → P (b x) (f x)) → P (′π , fold (a , b)) f) →
(∀ {a b x f} →
(∀ y → P (′w , fold (a , b)) (f y)) →
P (′w , fold (a , b)) (sup x f)) →
∀ u (x : El u) → P u x
U-rec P P1 P2t P2f Pσ Pπ Pw = rec
where
rec : ∀ u (x : El u) → P u x
rec (′0 , _) ()
rec (′1 , _) _ = P1
rec (′2 , _) true = P2t
rec (′2 , _) false = P2f
rec (′σ , fold (a , b)) (x , y) = Pσ (rec _ x) (rec _ y)
rec (′π , fold (a , b)) f = Pπ (λ x → rec _ (f x))
rec (′w , fold (a , b)) (fold (x , f)) = Pw (λ y → rec _ (f y))
```
The `--guardedness-preserving-type-constructors` extension is based
on a rather operational understanding of `∞`/`♯_`; it's not yet
clear if this extension is consistent.
* Qualified constructors.
Constructors can now be referred to qualified by their data type.
For instance, given
```agda
data Nat : Set where
zero : Nat
suc : Nat → Nat
data Fin : Nat → Set where
zero : ∀ {n} → Fin (suc n)
suc : ∀ {n} → Fin n → Fin (suc n)
```
you can refer to the constructors unambiguously as `Nat.zero`,
`Nat.suc`, `Fin.zero`, and `Fin.suc` (`Nat` and `Fin` are modules
containing the respective constructors). Example:
```agda
inj : (n m : Nat) → Nat.suc n ≡ suc m → n ≡ m
inj .m m refl = refl
```
Previously you had to write something like
```agda
inj : (n m : Nat) → _≡_ {Nat} (suc n) (suc m) → n ≡ m
```
to make the type checker able to figure out that you wanted the
natural number suc in this case.
* Reflection.
There are two new constructs for reflection:
- `quoteGoal x in e`
In `e` the value of `x` will be a representation of the goal type
(the type expected of the whole expression) as an element in a
datatype of Agda terms (see below). For instance,
```agda
example : ℕ
example = quoteGoal x in {! at this point x = def (quote ℕ) [] !}
```
- `quote x : Name`
If `x` is the name of a definition (function, datatype, record,
or a constructor), `quote x` gives you the representation of `x`
as a value in the primitive type `Name` (see below).
Quoted terms use the following BUILTINs and primitives (available
from the standard library module `Reflection`):
```agda
-- The type of Agda names.
postulate Name : Set
{-# BUILTIN QNAME Name #-}
primitive primQNameEquality : Name → Name → Bool
-- Arguments.
Explicit? = Bool
data Arg A : Set where
arg : Explicit? → A → Arg A
{-# BUILTIN ARG Arg #-}
{-# BUILTIN ARGARG arg #-}
-- The type of Agda terms.
data Term : Set where
var : ℕ → List (Arg Term) → Term
con : Name → List (Arg Term) → Term
def : Name → List (Arg Term) → Term
lam : Explicit? → Term → Term
pi : Arg Term → Term → Term
sort : Term
unknown : Term
{-# BUILTIN AGDATERM Term #-}
{-# BUILTIN AGDATERMVAR var #-}
{-# BUILTIN AGDATERMCON con #-}
{-# BUILTIN AGDATERMDEF def #-}
{-# BUILTIN AGDATERMLAM lam #-}
{-# BUILTIN AGDATERMPI pi #-}
{-# BUILTIN AGDATERMSORT sort #-}
{-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
```
Reflection may be useful when working with internal decision
procedures, such as the standard library's ring solver.
* Minor record definition improvement.
The definition of a record type is now available when type checking
record module definitions. This means that you can define things
like the following:
```agda
record Cat : Set₁ where
field
Obj : Set
_=>_ : Obj → Obj → Set
-- ...
-- not possible before:
op : Cat
op = record { Obj = Obj; _=>_ = λ A B → B => A }
```
Tools
-----
* The `Goal type and context` command now shows the goal type before
the context, and the context is shown in reverse order. The `Goal
type, context and inferred type` command has been modified in a
similar way.
* Show module contents command.
Given a module name `M` the Emacs mode can now display all the
top-level modules and names inside `M`, along with types for the
names. The command is activated using `C-c C-o` or the menus.
* Auto command.
A command which searches for type inhabitants has been added. The
command is invoked by pressing `C-C C-a` (or using the goal menu).
There are several flags and parameters, e.g. `-c` which enables
case-splitting in the search. For further information, see the Agda
wiki:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto
* HTML generation is now possible for a module with unsolved
meta-variables, provided that the `--allow-unsolved-metas` flag is
used.