Agda-2.8.0: doc/release-notes/2.4.2.md
Release notes for Agda version 2.4.2
====================================
Pragmas and options
-------------------
* New option: `--with-K`
This can be used to override a global `--without-K` in a file, by
adding a pragma `{-# OPTIONS --with-K #-}`.
* New pragma `{-# NON_TERMINATING #-}`
This is a safer version of `NO_TERMINATION_CHECK` which doesn't
treat the affected functions as terminating. This means that
`NON_TERMINATING` functions do not reduce during type checking. They
do reduce at run-time and when invoking `C-c C-n` at top-level (but
not in a hole).
Language
--------
* Instance search is now more efficient and recursive (see
Issue [#938](https://github.com/agda/agda/issues/938)) (but without
termination check yet).
A new keyword `instance` has been introduced (in the style of
`abstract` and `private`) which must now be used for every
definition/postulate that has to be taken into account during
instance resolution. For example:
```agda
record RawMonoid (A : Set) : Set where
field
nil : A
_++_ : A -> A -> A
open RawMonoid {{...}}
instance
rawMonoidList : {A : Set} -> RawMonoid (List A)
rawMonoidList = record { nil = []; _++_ = List._++_ }
rawMonoidMaybe : {A : Set} {{m : RawMonoid A}} -> RawMonoid (Maybe A)
rawMonoidMaybe {A} = record { nil = nothing ; _++_ = catMaybe }
where
catMaybe : Maybe A -> Maybe A -> Maybe A
catMaybe nothing mb = mb
catMaybe ma nothing = ma
catMaybe (just a) (just b) = just (a ++ b)
```
Moreover, each type of an instance must end in (something that reduces
to) a named type (e.g. a record, a datatype or a postulate). This
allows us to build a simple index structure
```
data/record name --> possible instances
```
that speeds up instance search.
Instance search takes into account all local bindings and all global
`instance` bindings and the search is recursive. For instance,
searching for
```agda
? : RawMonoid (Maybe (List A))
```
will consider the candidates {`rawMonoidList`, `rawMonoidMaybe`}, fail to
unify the first one, succeeding with the second one
```agda
? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A))
```
and continue with goal
```agda
?m : RawMonoid (List A)
```
This will then find
```agda
?m = rawMonoidList {A = A}
```
and putting together we have the solution.
Be careful that there is no termination check for now, you can
easily make Agda loop by declaring the identity function as an
instance. But it shouldn’t be possible to make Agda loop by only
declaring structurally recursive instances (whatever that means).
Additionally:
- Uniqueness of instances is up to definitional equality (see
Issue [#899](https://github.com/agda/agda/issues/899)).
- Instances of the following form are allowed:
```agda
EqSigma : {A : Set} {B : A → Set} {{EqA : Eq A}}
{{EqB : {a : A} → Eq (B a)}}
→ Eq (Σ A B)
```
When searching recursively for an instance of type `{a : A} → Eq
(B a)`, a lambda will automatically be introduced and instance
search will search for something of type `Eq (B a)` in the context
extended by `a : A`. When searching for an instance, the `a`
argument does not have to be implicit, but in the definition of
`EqSigma`, instance search will only be able to use `EqB` if `a`
is implicit.
- There is no longer any attempt to solve irrelevant metas by instance
search.
- Constructors of records and datatypes are automatically added to the
instance table.
* You can now use `quote` in patterns.
For instance, here is a function that unquotes a (closed) natural
number term.
```agda
unquoteNat : Term → Maybe Nat
unquoteNat (con (quote Nat.zero) []) = just zero
unquoteNat (con (quote Nat.suc) (arg _ n ∷ [])) = fmap suc (unquoteNat n)
unquoteNat _ = nothing
```
* The builtin constructors `AGDATERMUNSUPPORTED` and
`AGDASORTUNSUPPORTED` are now translated to meta variables when
unquoting.
* New syntactic sugar `tactic e` and `tactic e | e1 | .. | en`.
It desugars as follows and makes it less unwieldy to call
reflection-based tactics.
```agda
tactic e --> quoteGoal g in unquote (e g)
tactic e | e1 | .. | en --> quoteGoal g in unquote (e g) e1 .. en
```
Note that in the second form the tactic function should generate a
function from a number of new subgoals to the original goal. The
type of `e` should be `Term -> Term` in both cases.
* New reflection builtins for literals.
The term data type `AGDATERM` now needs an additional constructor
`AGDATERMLIT` taking a reflected literal defined as follows (with
appropriate builtin bindings for the types `Nat`, `Float`, etc).
```agda
data Literal : Set where
nat : Nat → Literal
float : Float → Literal
char : Char → Literal
string : String → Literal
qname : QName → Literal
{-# BUILTIN AGDALITERAL Literal #-}
{-# BUILTIN AGDALITNAT nat #-}
{-# BUILTIN AGDALITFLOAT float #-}
{-# BUILTIN AGDALITCHAR char #-}
{-# BUILTIN AGDALITSTRING string #-}
{-# BUILTIN AGDALITQNAME qname #-}
```
When quoting (`quoteGoal` or `quoteTerm`) literals will be mapped to
the `AGDATERMLIT` constructor. Previously natural number literals
were quoted to `suc`/`zero` application and other literals were
quoted to `AGDATERMUNSUPPORTED`.
* New reflection builtins for function definitions.
`AGDAFUNDEF` should now map to a data type defined as follows
(with
```agda
{-# BUILTIN QNAME QName #-}
{-# BUILTIN ARG Arg #-}
{-# BUILTIN AGDATERM Term #-}
{-# BUILTIN AGDATYPE Type #-}
{-# BUILTIN AGDALITERAL Literal #-}
```
).
```agda
data Pattern : Set where
con : QName → List (Arg Pattern) → Pattern
dot : Pattern
var : Pattern
lit : Literal → Pattern
proj : QName → Pattern
absurd : Pattern
{-# BUILTIN AGDAPATTERN Pattern #-}
{-# BUILTIN AGDAPATCON con #-}
{-# BUILTIN AGDAPATDOT dot #-}
{-# BUILTIN AGDAPATVAR var #-}
{-# BUILTIN AGDAPATLIT lit #-}
{-# BUILTIN AGDAPATPROJ proj #-}
{-# BUILTIN AGDAPATABSURD absurd #-}
data Clause : Set where
clause : List (Arg Pattern) → Term → Clause
absurd-clause : List (Arg Pattern) → Clause
{-# BUILTIN AGDACLAUSE Clause #-}
{-# BUILTIN AGDACLAUSECLAUSE clause #-}
{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
data FunDef : Set where
fun-def : Type → List Clause → FunDef
{-# BUILTIN AGDAFUNDEF FunDef #-}
{-# BUILTIN AGDAFUNDEFCON fun-def #-}
```
* New reflection builtins for extended (pattern-matching) lambda.
The `AGDATERM` data type has been augmented with a constructor
```agda
AGDATERMEXTLAM : List AGDACLAUSE → List (ARG AGDATERM) → AGDATERM
```
Absurd lambdas (`λ ()`) are quoted to extended lambdas with an
absurd clause.
* Unquoting declarations.
You can now define (recursive) functions by reflection using the new
`unquoteDecl` declaration
```agda
unquoteDecl x = e
```
Here e should have type `AGDAFUNDEF` and evaluate to a closed
value. This value is then spliced in as the definition of `x`. In
the body `e`, `x` has type `QNAME` which lets you splice in
recursive definitions.
Standard modifiers, such as fixity declarations, can be applied to `x` as
expected.
* Quoted levels
Universe levels are now quoted properly instead of being quoted to
`AGDASORTUNSUPPORTED`. `Setω` still gets an unsupported sort,
however.
* Module applicants can now be operator applications.
Example:
```agda
postulate
[_] : A -> B
module M (b : B) where
module N (a : A) = M [ a ]
```
[See Issue [#1245](https://github.com/agda/agda/issues/1245)]
* Minor change in module application
semantics. [Issue [#892](https://github.com/agda/agda/issues/892)]
Previously re-exported functions were not redefined when
instantiating a module. For instance
```agda
module A where f = ...
module B (X : Set) where
open A public
module C = B Nat
```
In this example `C.f` would be an alias for `A.f`, so if both `A`
and `C` were opened `f` would not be ambiguous. However, this
behaviour is not correct when `A` and `B` share some module
parameters
(Issue [#892](https://github.com/agda/agda/issues/892)). To fix this
`C` now defines its own copy of `f` (which evaluates to `A.f`),
which means that opening `A` and `C` results in an ambiguous `f`.
Type checking
-------------
* Recursive records need to be declared as either `inductive` or
`coinductive`. `inductive` is no longer default for recursive
records. Examples:
```agda
record _×_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
record Tree (A : Set) : Set where
inductive
constructor tree
field
elem : A
subtrees : List (Tree A)
record Stream (A : Set) : Set where
coinductive
constructor _::_
field
head : A
tail : Stream A
```
If you are using old-style (musical) coinduction, a record may have
to be declared as inductive, paradoxically.
```agda
record Stream (A : Set) : Set where
inductive -- YES, THIS IS INTENDED !
constructor _∷_
field
head : A
tail : ∞ (Stream A)
```
This is because the "coinduction" happens in the use of `∞` and not
in the use of `record`.
Tools
-----
### Emacs mode
* A new menu option `Display` can be used to display the version of
the running Agda process.
### LaTeX-backend
* New experimental option `references` has been added. When specified,
i.e.:
```latex
\usepackage[references]{agda}
```
a new command called `\AgdaRef` is provided, which lets you
reference previously typeset commands, e.g.:
Let us postulate `\AgdaRef{apa}`.
```agda
\begin{code}
postulate
apa : Set
\end{code}
```
Above `apa` will be typeset (highlighted) the same in the text as in
the code, provided that the LaTeX output is post-processed using
`src/data/postprocess-latex.pl`, e.g.:
```
cp $(dirname $(dirname $(agda-mode locate)))/postprocess-latex.pl .
agda -i. --latex Example.lagda
cd latex/
perl ../postprocess-latex.pl Example.tex > Example.processed
mv Example.processed Example.tex
xelatex Example.tex
```
Mix-fix and Unicode should work as expected (Unicode requires
XeLaTeX/LuaLaTeX), but there are limitations:
- Overloading identifiers should be avoided, if multiples exist
`\AgdaRef` will typeset according to the first it finds.
- Only the current module is used, should you need to reference
identifiers in other modules then you need to specify which other
module manually, i.e. `\AgdaRef[module]{identifier}`.