Agda-2.6.4: doc/release-notes/2.5.1.md
Release notes for Agda version 2.5.1
====================================
Documentation
-------------
* There is now an official Agda User Manual:
https://agda.readthedocs.io/
Installation and infrastructure
-------------------------------
* Builtins and primitives are now defined in a new set of modules available to
all users, independent of any particular library. The modules are
```agda
Agda.Builtin.Bool
Agda.Builtin.Char
Agda.Builtin.Coinduction
Agda.Builtin.Equality
Agda.Builtin.Float
Agda.Builtin.FromNat
Agda.Builtin.FromNeg
Agda.Builtin.FromString
Agda.Builtin.IO
Agda.Builtin.Int
Agda.Builtin.List
Agda.Builtin.Nat
Agda.Builtin.Reflection
Agda.Builtin.Size
Agda.Builtin.Strict
Agda.Builtin.String
Agda.Builtin.TrustMe
Agda.Builtin.Unit
```
The standard library reexports the primitives from the new modules.
The `Agda.Builtin` modules are installed in the same way as
`Agda.Primitive`, but unlike `Agda.Primitive` they are not loaded
automatically.
Pragmas and options
-------------------
* Library management
There is a new 'library' concept for managing include paths. A library
consists of
- a name,
- a set of libraries it depends on, and
- a set of include paths.
A library is defined in a `.agda-lib` file using the following
format:
```
name: LIBRARY-NAME -- Comment
depend: LIB1 LIB2
LIB3
LIB4
include: PATH1
PATH2
PATH3
```
Dependencies are library names, not paths to `.agda-lib` files, and
include paths are relative to the location of the library-file.
To be useable, a library file has to be listed (with its full path)
in `AGDA_DIR/libraries` (or `AGDA_DIR/libraries-VERSION`, for a
given Agda version). `AGDA_DIR` defaults to `~/.agda` on Unix-like
systems and `C:/Users/USERNAME/AppData/Roaming/agda` or similar on
Windows, and can be overridden by setting the `AGDA_DIR` environment
variable.
Environment variables in the paths (of the form `$VAR` or `${VAR}`)
are expanded. The location of the libraries file used can be
overridden using the `--library-file=FILE` flag, although this is
not expected to be very useful.
You can find out the precise location of the 'libraries' file by
calling `agda -l fjdsk Dummy.agda` and looking at the error message
(assuming you don't have a library called fjdsk installed).
There are three ways a library gets used:
- You supply the `--library=LIB` (or `-l LIB`) option to
Agda. This is equivalent to adding a `-iPATH` for each of the
include paths of `LIB` and its (transitive) dependencies.
- No explicit `--library` flag is given, and the current project
root (of the Agda file that is being loaded) or one of its
parent directories contains a `.agda-lib` file defining a
library `LIB`. This library is used as if a `--librarary=LIB`
option had been given, except that it is not necessary for the
library to be listed in the `AGDA_DIR/libraries` file.
- No explicit `--library` flag, and no `.agda-lib` file in the
project root. In this case the file `AGDA_DIR/defaults` is read
and all libraries listed are added to the path. The defaults
file should contain a list of library names, each on a separate
line. In this case the current directory is also added to the
path.
To disable default libraries, you can give the flag
`--no-default-libraries`.
Library names can end with a version number (for instance,
`mylib-1.2.3`). When resolving a library name (given in a `--library`
flag, or listed as a default library or library dependency) the
following rules are followed:
- If you don't give a version number, any version will do.
- If you give a version number an exact match is required.
- When there are multiple matches an exact match is preferred, and
otherwise the latest matching version is chosen.
For example, suppose you have the following libraries installed:
`mylib`, `mylib-1.0`, `otherlib-2.1`, and `otherlib-2.3`. In this
case, aside from the exact matches you can also say
`--library=otherlib` to get `otherlib-2.3`.
* New Pragma `COMPILED_DECLARE_DATA` for binding recursively defined
Haskell data types to recursively defined Agda data types.
If you have a Haskell type like
```haskell
{-# LANGUAGE GADTs #-}
module Issue223 where
data A where
BA :: B -> A
data B where
AB :: A -> B
BB :: B
```
You can now bind it to corresponding mutual Agda inductive data
types as follows:
```agda
{-# IMPORT Issue223 #-}
data A : Set
{-# COMPILED_DECLARE_DATA A Issue223.A #-}
data B : Set
{-# COMPILED_DECLARE_DATA B Issue223.B #-}
data A where
BA : B → A
{-# COMPILED_DATA A Issue223.A Issue223.BA #-}
data B where
AB : A → B
BB : B
{-# COMPILED_DATA B Issue223.B Issue223.AB Issue223.BB #-}
```
This fixes Issue [#223](https://github.com/agda/agda/issues/223).
* New pragma `HASKELL` for adding inline Haskell code (GHC backend only)
Arbitrary Haskell code can be added to a module using the `HASKELL`
pragma. For instance,
```agda
{-# HASKELL
echo :: IO ()
echo = getLine >>= putStrLn
#-}
postulate echo : IO ⊤
{-# COMPILED echo echo #-}
```
* New option `--exact-split`.
The `--exact-split` flag causes Agda to raise an error whenever a
clause in a definition by pattern matching cannot be made to hold
definitionally (i.e. as a reduction rule). Specific clauses can be
excluded from this check by means of the `{-# CATCHALL #-}` pragma.
For instance, the following definition will be rejected as the second clause
cannot be made to hold definitionally:
```agda
min : Nat → Nat → Nat
min zero y = zero
min x zero = zero
min (suc x) (suc y) = suc (min x y
```
Catchall clauses have to be marked as such, for instance:
```agda
eq : Nat → Nat → Bool
eq zero zero = true
eq (suc m) (suc n) = eq m n
{-# CATCHALL #-}
eq _ _ = false
```
* New option: `--no-exact-split`.
This option can be used to override a global `--exact-split` in a
file, by adding a pragma `{-# OPTIONS --no-exact-split #-}`.
* New options: `--sharing` and `--no-sharing`.
These options are used to enable/disable sharing and call-by-need
evaluation. The default is `--no-sharing`.
Note that they cannot appear in an `OPTIONS` pragma, but have to be
given as command line arguments or added to the Agda Program Args
from Emacs with `M-x customize-group agda2`.
* New pragma `DISPLAY`.
```agda
{-# DISPLAY f e1 .. en = e #-}
```
This causes `f e1 .. en` to be printed in the same way as `e`, where
`ei` can bind variables used in `e`. The expressions `ei` and `e`
are scope checked, but not type checked.
For example this can be used to print overloaded (instance) functions with
the overloaded name:
```agda
instance
NumNat : Num Nat
NumNat = record { ..; _+_ = natPlus }
{-# DISPLAY natPlus a b = a + b #-}
```
Limitations
- Left-hand sides are restricted to variables, constructors, defined
functions or types, and literals. In particular, lambdas are not
allowed in left-hand sides.
- Since `DISPLAY` pragmas are not type checked implicit argument
insertion may not work properly if the type of `f` computes to an
implicit function space after pattern matching.
* Removed pragma `{-# ETA R #-}`
The pragma `{-# ETA R #-}` is replaced by the `eta-equality` directive
inside record declarations.
* New option `--no-eta-equality`.
The `--no-eta-equality` flag disables eta rules for declared record
types. It has the same effect as `no-eta-equality` inside each
declaration of a record type `R`.
If used with the `OPTIONS` pragma it will not affect records defined
in other modules.
* The semantics of `{-# REWRITE r #-}` pragmas in parametrized modules
has changed (see
Issue [#1652](https://github.com/agda/agda/issues/1652)).
Rewrite rules are no longer lifted to the top context. Instead, they
now only apply to terms in (extensions of) the module context. If
you want the old behaviour, you should put the `{-# REWRITE r #-}`
pragma outside of the module (i.e. unindent it).
* New pragma `{-# INLINE f #-}` causes `f` to be inlined during
compilation.
* The `STATIC` pragma is now taken into account during compilation.
Calls to a function marked `STATIC` are normalised before
compilation. The typical use case for this is to mark the
interpreter of an embedded language as `STATIC`.
* Option `--type-in-type` no longer implies
`--no-universe-polymorphism`, thus, it can be used with explicit
universe
levels. [Issue [#1764](https://github.com/agda/agda/issues/1764)] It
simply turns off error reporting for any level mismatch now.
Examples:
```agda
{-# OPTIONS --type-in-type #-}
Type : Set
Type = Set
data D {α} (A : Set α) : Set where
d : A → D A
data E α β : Set β where
e : Set α → E α β
```
* New `NO_POSITIVITY_CHECK` pragma to switch off the positivity checker
for data/record definitions and mutual blocks.
The pragma must precede a data/record definition or a mutual block.
The pragma cannot be used in `--safe` mode.
Examples (see `Issue1614*.agda` and `Issue1760*.agda` in
`test/Succeed/`):
1. Skipping a single data definition.
```agda
{-# NO_POSITIVITY_CHECK #-}
data D : Set where
lam : (D → D) → D
```
2. Skipping a single record definition.
```agda
{-# NO_POSITIVITY_CHECK #-}
record U : Set where
field ap : U → U
```
3. Skipping an old-style mutual block: Somewhere within a `mutual`
block before a data/record definition.
```agda
mutual
data D : Set where
lam : (D → D) → D
{-# NO_POSITIVITY_CHECK #-}
record U : Set where
field ap : U → U
```
4. Skipping an old-style mutual block: Before the `mutual` keyword.
```agda
{-# NO_POSITIVITY_CHECK #-}
mutual
data D : Set where
lam : (D → D) → D
record U : Set where
field ap : U → U
```
5. Skipping a new-style mutual block: Anywhere before the
declaration or the definition of data/record in the block.
```agda
record U : Set
data D : Set
record U where
field ap : U → U
{-# NO_POSITIVITY_CHECK #-}
data D where
lam : (D → D) → D
```
* Removed `--no-coverage-check`
option. [Issue [#1918](https://github.com/agda/agda/issues/1918)]
Language
--------
### Operator syntax
* The default fixity for syntax declarations has changed from -666 to 20.
* Sections.
Operators can be sectioned by replacing arguments with underscores.
There must not be any whitespace between these underscores and the
adjacent nameparts. Examples:
```agda
pred : ℕ → ℕ
pred = _∸ 1
T : Bool → Set
T = if_then ⊤ else ⊥
if : {A : Set} (b : Bool) → A → A → A
if b = if b then_else_
```
Sections are translated into lambda expressions. Examples:
```agda
_∸ 1 ↦ λ section → section ∸ 1
if_then ⊤ else ⊥ ↦ λ section → if section then ⊤ else ⊥
if b then_else_ ↦ λ section section₁ →
if b then section else section₁
```
Operator sections have the same fixity as the underlying operator
(except in cases like `if b then_else_`, in which the section is
"closed", but the operator is not).
Operator sections are not supported in patterns (with the exception
of dot patterns), and notations coming from syntax declarations
cannot be sectioned.
* A long-standing operator fixity bug has been fixed. As a consequence
some programs that used to parse no longer do.
Previously each precedence level was (incorrectly) split up into
five separate ones, ordered as follows, with the earlier ones
binding less tightly than the later ones:
- Non-associative operators.
- Left associative operators.
- Right associative operators.
- Prefix operators.
- Postfix operators.
Now this problem has been addressed. It is no longer possible to mix
operators of a given precedence level but different associativity.
However, prefix and right associative operators are seen as having
the same associativity, and similarly for postfix and left
associative operators.
Examples
--------
The following code is no longer accepted:
```agda
infixl 6 _+_
infix 6 _∸_
rejected : ℕ
rejected = 1 + 0 ∸ 1
```
However, the following previously rejected code is accepted:
```agda
infixr 4 _,_
infix 4 ,_
,_ : {A : Set} {B : A → Set} {x : A} → B x → Σ A B
, y = _ , y
accepted : Σ ℕ λ i → Σ ℕ λ j → Σ (i ≡ j) λ _ → Σ ℕ λ k → j ≡ k
accepted = 5 , , refl , , refl
```
* The classification of notations with binders into the categories
infix, prefix, postfix or closed has
changed. [Issue [#1450](https://github.com/agda/agda/issues/1450)]
The difference is that, when classifying the notation, only
*regular* holes are taken into account, not *binding* ones.
Example: The notation
```agda
syntax m >>= (λ x → f) = x <- m , f
```
was previously treated as infix, but is now treated as prefix.
* Notation can now include wildcard binders.
Example: `syntax Σ A (λ _ → B) = A × B`
* If an overloaded operator is in scope with several distinct
precedence levels, then several instances of this operator will be
included in the operator grammar, possibly leading to ambiguity.
Previously the operator was given the default fixity
[Issue [#1436](https://github.com/agda/agda/issues/1436)].
There is an exception to this rule: If there are multiple precedences,
but at most one is explicitly declared, then only one instance will be
included in the grammar. If there are no explicitly declared
precedences, then this instance will get the default precedence, and
otherwise it will get the declared precedence.
If multiple occurrences of an operator are "merged" in the grammar,
and they have distinct associativities, then they are treated as
being non-associative.
The three paragraphs above also apply to identical notations (coming
from syntax declarations) for a given overloaded name.
Examples:
```agda
module A where
infixr 5 _∷_
infixr 5 _∙_
infixl 3 _+_
infix 1 bind
syntax bind c (λ x → d) = x ← c , d
module B where
infix 5 _∷_
infixr 4 _∙_
-- No fixity declaration for _+_.
infixl 2 bind
syntax bind c d = c ∙ d
module C where
infixr 2 bind
syntax bind c d = c ∙ d
open A
open B
open C
-- _∷_ is infix 5.
-- _∙_ has two fixities: infixr 4 and infixr 5.
-- _+_ is infixl 3.
-- A.bind's notation is infix 1.
-- B.bind and C.bind's notations are infix 2.
-- There is one instance of "_ ∷ _" in the grammar, and one
-- instance of "_ + _".
-- There are three instances of "_ ∙ _" in the grammar, one
-- corresponding to A._∙_, one corresponding to B._∙_, and one
-- corresponding to both B.bind and C.bind.
```
### Reflection
* The reflection framework has received a massive overhaul.
A new type of reflected type checking computations supplants most of
the old reflection primitives. The `quoteGoal`, `quoteContext` and
tactic primitives are deprecated and will be removed in the future,
and the `unquoteDecl` and `unquote` primitives have changed
behaviour. Furthermore the following primitive functions have been
replaced by builtin type checking computations:
```agda
- primQNameType --> AGDATCMGETTYPE
- primQNameDefinition --> AGDATCMGETDEFINITION
- primDataConstructors --> subsumed by AGDATCMGETDEFINITION
- primDataNumberOfParameters --> subsumed by AGDATCMGETDEFINITION
```
See below for details.
* Types are no longer packaged with a sort.
The `AGDATYPE` and `AGDATYPEEL` built-ins have been
removed. Reflected types are now simply terms.
* Reflected definitions have more information.
The type for reflected definitions has changed to
```agda
data Definition : Set where
fun-def : List Clause → Definition
data-type : Nat → List Name → Definition -- parameters and constructors
record-type : Name → Definition -- name of the data/record type
data-con : Name → Definition -- name of the constructor
axiom : Definition
prim-fun : Definition
```
Correspondingly the built-ins for function, data and record
definitions (`AGDAFUNDEF`, `AGDAFUNDEFCON`, `AGDADATADEF`,
`AGDARECORDDEF`) have been removed.
* Reflected type checking computations.
There is a primitive `TC` monad representing type checking
computations. The `unquote`, `unquoteDecl`, and the new `unquoteDef`
all expect computations in this monad (see below). The interface to
the monad is the following
```agda
-- Error messages can contain embedded names and terms.
data ErrorPart : Set where
strErr : String → ErrorPart
termErr : Term → ErrorPart
nameErr : Name → ErrorPart
{-# BUILTIN AGDAERRORPART ErrorPart #-}
{-# BUILTIN AGDAERRORPARTSTRING strErr #-}
{-# BUILTIN AGDAERRORPARTTERM termErr #-}
{-# BUILTIN AGDAERRORPARTNAME nameErr #-}
postulate
TC : ∀ {a} → Set a → Set a
returnTC : ∀ {a} {A : Set a} → A → TC A
bindTC : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
-- Unify two terms, potentially solving metavariables in the process.
unify : Term → Term → TC ⊤
-- Throw a type error. Can be caught by catchTC.
typeError : ∀ {a} {A : Set a} → List ErrorPart → TC A
-- Block a type checking computation on a metavariable. This will abort
-- the computation and restart it (from the beginning) when the
-- metavariable is solved.
blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A
-- Backtrack and try the second argument if the first argument throws a
-- type error.
catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A
-- Infer the type of a given term
inferType : Term → TC Type
-- Check a term against a given type. This may resolve implicit arguments
-- in the term, so a new refined term is returned. Can be used to create
-- new metavariables: newMeta t = checkType unknown t
checkType : Term → Type → TC Term
-- Compute the normal form of a term.
normalise : Term → TC Term
-- Get the current context.
getContext : TC (List (Arg Type))
-- Extend the current context with a variable of the given type.
extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A
-- Set the current context.
inContext : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A
-- Quote a value, returning the corresponding Term.
quoteTC : ∀ {a} {A : Set a} → A → TC Term
-- Unquote a Term, returning the corresponding value.
unquoteTC : ∀ {a} {A : Set a} → Term → TC A
-- Create a fresh name.
freshName : String → TC QName
-- Declare a new function of the given type. The function must be defined
-- later using 'defineFun'. Takes an Arg Name to allow declaring instances
-- and irrelevant functions. The Visibility of the Arg must not be hidden.
declareDef : Arg QName → Type → TC ⊤
-- Define a declared function. The function may have been declared using
-- 'declareDef' or with an explicit type signature in the program.
defineFun : QName → List Clause → TC ⊤
-- Get the type of a defined name. Replaces 'primQNameType'.
getType : QName → TC Type
-- Get the definition of a defined name. Replaces 'primQNameDefinition'.
getDefinition : QName → TC Definition
{-# BUILTIN AGDATCM TC #-}
{-# BUILTIN AGDATCMRETURN returnTC #-}
{-# BUILTIN AGDATCMBIND bindTC #-}
{-# BUILTIN AGDATCMUNIFY unify #-}
{-# BUILTIN AGDATCMNEWMETA newMeta #-}
{-# BUILTIN AGDATCMTYPEERROR typeError #-}
{-# BUILTIN AGDATCMBLOCKONMETA blockOnMeta #-}
{-# BUILTIN AGDATCMCATCHERROR catchTC #-}
{-# BUILTIN AGDATCMINFERTYPE inferType #-}
{-# BUILTIN AGDATCMCHECKTYPE checkType #-}
{-# BUILTIN AGDATCMNORMALISE normalise #-}
{-# BUILTIN AGDATCMGETCONTEXT getContext #-}
{-# BUILTIN AGDATCMEXTENDCONTEXT extendContext #-}
{-# BUILTIN AGDATCMINCONTEXT inContext #-}
{-# BUILTIN AGDATCMQUOTETERM quoteTC #-}
{-# BUILTIN AGDATCMUNQUOTETERM unquoteTC #-}
{-# BUILTIN AGDATCMFRESHNAME freshName #-}
{-# BUILTIN AGDATCMDECLAREDEF declareDef #-}
{-# BUILTIN AGDATCMDEFINEFUN defineFun #-}
{-# BUILTIN AGDATCMGETTYPE getType #-}
{-# BUILTIN AGDATCMGETDEFINITION getDefinition #-}
```
* Builtin type for metavariables
There is a new builtin type for metavariables used by the new reflection
framework. It is declared as follows and comes with primitive equality,
ordering and show.
```agda
postulate Meta : Set
{-# BUILTIN AGDAMETA Meta #-}
primitive primMetaEquality : Meta → Meta → Bool
primitive primMetaLess : Meta → Meta → Bool
primitive primShowMeta : Meta → String
```
There are corresponding new constructors in the `Term` and `Literal`
data types:
```agda
data Term : Set where
...
meta : Meta → List (Arg Term) → Term
{-# BUILTIN AGDATERMMETA meta #-}
data Literal : Set where
...
meta : Meta → Literal
{-# BUILTIN AGDALITMETA meta #-}
```
* Builtin unit type
The type checker needs to know about the unit type, which you can
allow by
```agda
record ⊤ : Set where
{-# BUILTIN UNIT ⊤ #-}
```
* Changed behaviour of `unquote`
The `unquote` primitive now expects a type checking computation
instead of a pure term. In particular `unquote e` requires
```agda
e : Term → TC ⊤
```
where the argument is the representation of the hole in which the
result should go. The old `unquote` behaviour (where `unquote`
expected a `Term` argument) can be recovered by
```agda
OLD: unquote v
NEW: unquote λ hole → unify hole v
```
* Changed behaviour of `unquoteDecl`
The `unquoteDecl` primitive now expects a type checking computation
instead of a pure function definition. It is possible to define
multiple (mutually recursive) functions at the same time. More
specifically
```agda
unquoteDecl x₁ .. xₙ = m
```
requires `m : TC ⊤` and that `x₁ .. xₙ` are defined (using
`declareDef` and `defineFun`) after executing `m`. As before `x₁
.. xₙ : QName` in `m`, but have their declared types outside the
`unquoteDecl`.
* New primitive `unquoteDef`
There is a new declaration
```agda
unquoteDef x₁ .. xₙ = m
```
This works exactly as `unquoteDecl` (see above) with the exception
that `x₁ .. xₙ` are required to already be declared.
The main advantage of `unquoteDef` over `unquoteDecl` is that
`unquoteDef` is allowed in mutual blocks, allowing mutually
recursion between generated definitions and hand-written
definitions.
* The reflection interface now exposes the name hint (as a string)
for variables. As before, the actual binding structure is with
de Bruijn indices. The String value is just a hint used as a prefix
to help display the variable. The type `Abs` is a new builtin type used
for the constructors `Term.lam`, `Term.pi`, `Pattern.var`
(bultins `AGDATERMLAM`, `AGDATERMPI` and `AGDAPATVAR`).
```agda
data Abs (A : Set) : Set where
abs : (s : String) (x : A) → Abs A
{-# BUILTIN ABS Abs #-}
{-# BUILTIN ABSABS abs #-}
```
Updated constructor types:
```agda
Term.lam : Hiding → Abs Term → Term
Term.pi : Arg Type → Abs Type → Term
Pattern.var : String → Pattern
```
* Reflection-based macros
Macros are functions of type `t1 → t2 → .. → Term → TC ⊤` that are
defined in a `macro` block. Macro application is guided by the type
of the macro, where `Term` arguments desugar into the `quoteTerm`
syntax and `Name` arguments into the `quote` syntax. Arguments of
any other type are preserved as-is. The last `Term` argument is the
hole term given to `unquote` computation (see above).
For example, the macro application `f u v w` where the macro `f` has
the type `Term → Name → Bool → Term → TC ⊤` desugars into `unquote
(f (quoteTerm u) (quote v) w)`
Limitations:
- Macros cannot be recursive. This can be worked around by defining the
recursive function outside the macro block and have the macro call the
recursive function.
Silly example:
```agda
macro
plus-to-times : Term → Term → TC ⊤
plus-to-times (def (quote _+_) (a ∷ b ∷ [])) hole = unify hole (def (quote _*_) (a ∷ b ∷ []))
plus-to-times v hole = unify hole v
thm : (a b : Nat) → plus-to-times (a + b) ≡ a * b
thm a b = refl
```
Macros are most useful when writing tactics, since they let you hide the
reflection machinery. For instance, suppose you have a solver
```agda
magic : Type → Term
```
that takes a reflected goal and outputs a proof (when successful). You can
then define the following macro
```agda
macro
by-magic : Term → TC ⊤
by-magic hole =
bindTC (inferType hole) λ goal →
unify hole (magic goal)
```
This lets you apply the magic tactic without any syntactic noise at all:
```agda
thm : ¬ P ≡ NP
thm = by-magic
```
### Literals and built-ins
* Overloaded number literals.
You can now overload natural number literals using the new builtin
`FROMNAT`:
```agda
{-# BUILTIN FROMNAT fromNat #-}
```
The target of the builtin should be a defined name. Typically you would do
something like
```agda
record Number (A : Set) : Set where
field fromNat : Nat → A
open Number {{...}} public
{-# BUILTIN FROMNAT fromNat #-}
```
This will cause number literals `n` to be desugared to `fromNat n`
before type checking.
* Negative number literals.
Number literals can now be negative. For floating point literals it
works as expected. For integer literals there is a new builtin
`FROMNEG` that enables negative integer literals:
```agda
{-# BUILTIN FROMNEG fromNeg #-}
```
This causes negative literals `-n` to be desugared to `fromNeg n`.
* Overloaded string literals.
String literals can be overladed using the `FROMSTRING` builtin:
```agda
{-# BUILTIN FROMSTRING fromString #-}
```
The will cause string literals `s` to be desugared to `fromString s`
before type checking.
* Change to builtin integers.
The `INTEGER` builtin now needs to be bound to a datatype with two
constructors that should be bound to the new builtins `INTEGERPOS`
and `INTEGERNEGSUC` as follows:
```agda
data Int : Set where
pos : Nat -> Int
negsuc : Nat -> Int
{-# BUILTIN INTEGER Int #-}
{-# BUILTIN INTEGERPOS pos #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}
```
where `negsuc n` represents the integer `-n - 1`. For instance, `-5`
is represented as `negsuc 4`. All primitive functions on integers
except `primShowInteger` have been removed, since these can be
defined without too much trouble on the above representation using
the corresponding functions on natural numbers.
The primitives that have been removed are
```agda
primIntegerPlus
primIntegerMinus
primIntegerTimes
primIntegerDiv
primIntegerMod
primIntegerEquality
primIntegerLess
primIntegerAbs
primNatToInteger
```
* New primitives for strict evaluation
```agda
primitive
primForce : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x
```
`primForce x f` evaluates to `f x` if x is in weak head normal form,
and `primForceLemma x f` evaluates to `refl` in the same
situation. The following values are considered to be in weak head
normal form:
- constructor applications
- literals
- lambda abstractions
- type constructor (data/record types) applications
- function types
- Set a
### Modules
* Modules in import directives
When you use `using`/`hiding`/`renaming` on a name it now
automatically applies to any module of the same name, unless you
explicitly mention the module. For instance,
```agda
open M using (D)
```
is equivalent to
```agda
open M using (D; module D)
```
if `M` defines a module `D`. This is most useful for record and data
types where you always get a module of the same name as the type.
With this feature there is no longer useful to be able to qualify a
constructor (or field) by the name of the data type even when it
differs from the name of the corresponding module. The follow
(weird) code used to work, but doesn't work anymore:
```agda
module M where
data D where
c : D
open M using (D) renaming (module D to MD)
foo : D
foo = D.c
```
If you want to import only the type name and not the module you have to hide
it explicitly:
```agda
open M using (D) hiding (module D)
```
See discussion on
Issue [#836](https://github.com/agda/agda/issues/836).
* Private definitions of a module are no longer in scope at the Emacs
mode top-level.
The reason for this change is that `.agdai-files` are stripped of
unused private definitions (which can yield significant performance
improvements for module-heavy code).
To test private definitions you can create a hole at the bottom of
the module, in which private definitions will be visible.
### Records
* New record directives `eta-equality`/`no-eta-equality`
The keywords `eta-equality`/`no-eta-equality` enable/disable eta
rules for the (inductive) record type being declared.
```agda
record Σ (A : Set) (B : A -> Set) : Set where
no-eta-equality
constructor _,_
field
fst : A
snd : B fst
open Σ
-- fail : ∀ {A : Set}{B : A -> Set} → (x : Σ A B) → x ≡ (fst x , snd x)
-- fail x = refl
--
-- x != fst x , snd x of type Σ .A .B
-- when checking that the expression refl has type x ≡ (fst x , snd x)
```
* Building records from modules.
The `record { <fields> }` syntax is now extended to accept module
names as well. Fields are thus defined using the corresponding
definitions from the given module.
For instance assuming this record type `R` and module `M`:
```agda
record R : Set where
field
x : X
y : Y
z : Z
module M where
x = {! ... !}
y = {! ... !}
r : R
r = record { M; z = {! ... !} }
```
Previously one had to write `record { x = M.x; y = M.y; z = {! ... !} }`.
More precisely this construction now supports any combination of explicit
field definitions and applied modules.
If a field is both given explicitly and available in one of the modules,
then the explicit one takes precedence.
If a field is available in more than one module then this is ambiguous
and therefore rejected. As a consequence the order of assignments does
not matter.
The modules can be both applied to arguments and have import directives
such as `hiding`, `using`, and `renaming`. In particular this construct
subsumes the record update construction.
Here is an example of record update:
```agda
-- Record update. Same as: record r { y = {! ... !} }
r2 : R
r2 = record { R r; y = {! ... !} }
```
A contrived example showing the use of `hiding`/`renaming`:
```agda
module M2 (a : A) where
w = {! ... !}
z = {! ... !}
r3 : A → R
r3 a = record { M hiding (y); M2 a renaming (w to y) }
```
* Record patterns are now accepted.
Examples:
```agda
swap : {A B : Set} (p : A × B) → B × A
swap record{ proj₁ = a; proj₂ = b } = record{ proj₁ = b; proj₂ = a }
thd3 : ...
thd3 record{ proj₂ = record { proj₂ = c }} = c
```
* Record modules now properly hide all their parameters
[Issue [#1759](https://github.com/agda/agda/issues/1759)]
Previously parameters to parent modules were not hidden in the record
module, resulting in different behaviour between
```agda
module M (A : Set) where
record R (B : Set) : Set where
```
and
```agda
module M where
record R (A B : Set) : Set where
```
where in the former case, `A` would be an explicit argument to the module
`M.R`, but implicit in the latter case. Now `A` is implicit in both cases.
### Instance search
* Performance has been improved, recursive instance search which was
previously exponential in the depth is now only quadratic.
* Constructors of records and datatypes are not anymore automatically
considered as instances, you have to do so explicitely, for
instance:
```agda
-- only [b] is an instance of D
data D : Set where
a : D
instance
b : D
c : D
-- the constructor is now an instance
record tt : Set where
instance constructor tt
```
* Lambda-bound variables are no longer automatically considered
instances.
Lambda-bound variables need to be bound as instance arguments to be
considered for instance search. For example,
```agda
_==_ : {A : Set} {{_ : Eq A}} → A → A → Bool
fails : {A : Set} → Eq A → A → Bool
fails eqA x = x == x
works : {A : Set} {{_ : Eq A}} → A → Bool
works x = x == x
```
* Let-bound variables are no longer automatically considered
instances.
To make a let-bound variable available as an instance it needs to be
declared with the `instance` keyword, just like top-level
instances. For example,
```agda
mkEq : {A : Set} → (A → A → Bool) → Eq A
fails : {A : Set} → (A → A → Bool) → A → Bool
fails eq x = let eqA = mkEq eq in x == x
works : {A : Set} → (A → A → Bool) → A → Bool
works eq x = let instance eqA = mkEq eq in x == x
```
* Record fields can be declared instances.
For example,
```agda
record EqSet : Set₁ where
field
set : Set
instance eq : Eq set
```
This causes the projection function `eq : (E : EqSet) → Eq (set E)`
to be considered for instance search.
* Instance search can now find arguments in variable types (but such
candidates can only be lambda-bound variables, they can’t be
declared as instances)
```agda
module _ {A : Set} (P : A → Set) where
postulate
bla : {x : A} {{_ : P x}} → Set → Set
-- Works, the instance argument is found in the context
test : {x : A} {{_ : P x}} → Set → Set
test B = bla B
-- Still forbidden, because [P] could be instantiated later to anything
instance
postulate
forbidden : {x : A} → P x
```
* Instance search now refuses to solve constraints with unconstrained
metavariables, since this can lead to non-termination.
See [Issue [#1532](https://github.com/agda/agda/issues/1523)] for an
example.
* Top-level instances are now only considered if they are in
scope. [Issue [#1913](https://github.com/agda/agda/issues/1913)]
Note that lambda-bound instances need not be in scope.
### Other changes
* Unicode ellipsis character is allowed for the ellipsis token `...`
in `with` expressions.
* `Prop` is no longer a reserved word.
Type checking
-------------
* Large indices.
Force constructor arguments no longer count towards the size of a datatype.
For instance, the definition of equality below is accepted.
```agda
data _≡_ {a} {A : Set a} : A → A → Set where
refl : ∀ x → x ≡ x
```
This gets rid of the asymmetry that the version of equality which indexes
only on the second argument could be small, but not the version above which
indexes on both arguments.
* Detection of datatypes that satisfy K (i.e. sets)
Agda will now try to detect datatypes that satisfy K when
`--without-K` is enabled. A datatype satisfies K when it follows
these three rules:
- The types of all non-recursive constructor arguments should satisfy K.
- All recursive constructor arguments should be first-order.
- The types of all indices should satisfy K.
For example, the types `Nat`, `List Nat`, and `x ≡ x` (where `x :
Nat`) are all recognized by Agda as satisfying K.
* New unifier for case splitting
The unifier used by Agda for case splitting has been completely
rewritten. The new unifier takes a much more type-directed approach
in order to avoid the problems in issues
[#1406](https://github.com/agda/agda/issues/1406),
[#1408](https://github.com/agda/agda/issues/1408),
[#1427](https://github.com/agda/agda/issues/1427), and
[#1435](https://github.com/agda/agda/issues/1435).
The new unifier also has eta-equality for record types
built-in. This should avoid unnecessary case splitting on record
constructors and improve the performance of Agda on code that
contains deeply nested record patterns (see issues
[#473](https://github.com/agda/agda/issues/473),
[#635](https://github.com/agda/agda/issues/635),
[#1575](https://github.com/agda/agda/issues/1575),
[#1603](https://github.com/agda/agda/issues/1603),
[#1613](https://github.com/agda/agda/issues/1613), and
[#1645](https://github.com/agda/agda/issues/1645)).
In some cases, the locations of the dot patterns computed by the
unifier did not correspond to the locations given by the user (see
Issue [#1608](https://github.com/agda/agda/issues/1608)). This has
now been fixed by adding an extra step after case splitting that
checks whether the user-written patterns are compatible with the
computed ones.
In some rare cases, the new unifier is still too restrictive when
`--without-K` is enabled because it cannot generalize over the
datatype indices (yet). For example, the following code is rejected:
```agda
data Bar : Set₁ where
bar : Bar
baz : (A : Set) → Bar
data Foo : Bar → Set where
foo : Foo bar
test : foo ≡ foo → Set₁
test refl = Set
```
* The aggressive behaviour of `with` introduced in 2.4.2.5 has been
rolled back
[Issue [#1692](https://github.com/agda/agda/issues/1692)]. With no
longer abstracts in the types of variables appearing in the
with-expressions. [Issue [#745](https://github.com/agda/agda/issues/745)]
This means that the following example no longer works:
```agda
fails : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
fails f b with a | f b
fails f b | .b | refl = f b
```
The `with` no longer abstracts the type of `f` over `a`, since `f`
appears in the second with-expression `f b`. You can use a nested
`with` to make this example work.
This example does work again:
```agda
test : ∀{A : Set}{a : A}{f : A → A} (p : f a ≡ a) → f (f a) ≡ a
test p rewrite p = p
```
After `rewrite p` the goal has changed to `f a ≡ a`, but the type
of `p` has not been rewritten, thus, the final `p` solves the goal.
The following, which worked in 2.4.2.5, no longer works:
```agda
fails : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
fails f b rewrite f b = f b
```
The rewrite with `f b : a ≡ b` is not applied to `f` as
the latter is part of the rewrite expression `f b`. Thus,
the type of `f` remains untouched, and the changed goal
`b ≡ b` is not solved by `f b`.
* When using `rewrite` on a term `eq` of type `lhs ≡ rhs`, the `lhs`
is no longer abstracted in `rhs`
[Issue [#520](https://github.com/agda/agda/issues/520)]. This means
that
```agda
f pats rewrite eq = body
```
is more than syntactic sugar for
```agda
f pats with lhs | eq
f pats | _ | refl = body
```
In particular, the following application of `rewrite` is now
possible
```agda
id : Bool → Bool
id true = true
id false = false
is-id : ∀ x → x ≡ id x
is-id true = refl
is-id false = refl
postulate
P : Bool → Set
b : Bool
p : P (id b)
proof : P b
proof rewrite is-id b = p
```
Previously, this was desugared to
```agda
proof with b | is-id b
proof | _ | refl = p
```
which did not type check as `refl` does not have type `b ≡ id b`.
Now, Agda gets the task of checking `refl : _ ≡ id b` leading to
instantiation of `_` to `id b`.
Compiler backends
-----------------
* Major Bug Fixes:
- Function clauses with different arities are now always compiled
correctly by the GHC/UHC
backends. (Issue [#727](https://github.com/agda/agda/issues/727))
* Co-patterns
- The GHC/UHC backends now support co-patterns. (Issues
[#1567](https://github.com/agda/agda/issues/1567),
[#1632](https://github.com/agda/agda/issues/1632))
* Optimizations
- Builtin naturals are now represented as arbitrary-precision
Integers. See the user manual, section
"Agda Compilers -> Optimizations" for details.
* GHC Haskell backend (MAlonzo)
- Pragmas
Since builtin naturals are compiled to `Integer` you can no longer
give a `{-# COMPILED_DATA #-}` pragma for `Nat`. The same goes for
builtin booleans, integers, floats, characters and strings which
are now hard-wired to appropriate Haskell types.
* UHC compiler backend
A new backend targeting the Utrecht Haskell Compiler (UHC) is
available. It targets the UHC Core language, and it's design is
inspired by the Epic backend. See the user manual, section "Agda
Compilers -> UHC Backend" for installation instructions.
- FFI
The UHC backend has a FFI to Haskell similar to MAlonzo's. The
target Haskell code also needs to be compilable using UHC, which
does not support the Haskell base library version 4.*.
FFI pragmas for the UHC backend are not checked in any way. If the
pragmas are wrong, bad things will happen.
- Imports
Additional Haskell modules can be brought into scope with the
`IMPORT_UHC` pragma:
```agda
{-# IMPORT_UHC Data.Char #-}
```
The Haskell modules `UHC.Base` and `UHC.Agda.Builtins` are always in
scope and don't need to be imported explicitly.
- Datatypes
Agda datatypes can be bound to Haskell datatypes as follows:
Haskell:
```haskell
data HsData a = HsCon1 | HsCon2 (HsData a)
```
Agda:
```agda
data AgdaData (A : Set) : Set where
AgdaCon1 : AgdaData A
AgdaCon2 : AgdaData A -> AgdaData A
{-# COMPILED_DATA_UHC AgdaData HsData HsCon1 HsCon2 #-}
```
The mapping has to cover all constructors of the used Haskell
datatype, else runtime behavior is undefined!
There are special reserved names to bind Agda datatypes to certain
Haskell datatypes. For example, this binds an Agda datatype to
Haskell's list datatype:
Agda:
```agda
data AgdaList (A : Set) : Set where
Nil : AgdaList A
Cons : A -> AgdaList A -> AgdaList A
{-# COMPILED_DATA_UHC AgdaList __LIST__ __NIL__ __CONS__ #-}
```
The following "magic" datatypes are available:
```
HS Datatype | Datatype Pragma | HS Constructor | Constructor Pragma
() __UNIT__ () __UNIT__
List __LIST__ (:) __CONS__
[] __NIL__
Bool __BOOL__ True __TRUE__
False __FALSE__
```
- Functions
Agda postulates can be bound to Haskell functions. Similar as in
MAlonzo, all arguments of type `Set` need to be dropped before
calling Haskell functions. An example calling the return function:
Agda:
```agda
postulate hs-return : {A : Set} -> A -> IO A
{-# COMPILED_UHC hs-return (\_ -> UHC.Agda.Builtins.primReturn) #-}
```
Emacs mode and interaction
--------------------------
* Module contents (`C-c C-o`) now also works for
records. [See Issue [#1926](https://github.com/agda/agda/issues/1926) ]
If you have an inferable expression of record type in an interaction
point, you can invoke `C-c C-o` to see its fields and types.
Example
```agda
record R : Set where
field f : A
test : R → R
test r = {!r!} -- C-c C-o here
```
* Less aggressive error notification.
Previously Emacs could jump to the position of an error even if the
type-checking process was not initiated in the current buffer. Now
this no longer happens: If the type-checking process was initiated
in another buffer, then the cursor is moved to the position of the
error in the buffer visiting the file (if any) and in every window
displaying the file, but focus should not change from one file to
another.
In the cases where focus does change from one file to another, one
can now use the go-back functionality to return to the previous
position.
* Removed the `agda-include-dirs` customization parameter.
Use `agda-program-args` with `-iDIR` or `-lLIB` instead, or add
libraries to `~/.agda/defaults`
(`C:/Users/USERNAME/AppData/Roaming/agda/defaults` or similar on
Windows). See Library management, above, for more information.
Tools
-----
### LaTeX-backend
* The default font has been changed to XITS (which is part of TeX Live):
http://www.ctan.org/tex-archive/fonts/xits/
This font is more complete with respect to Unicode.
### agda-ghc-names
* New tool: The command
```
agda-ghc-names fixprof <compile-dir> <ProgName>.prof
```
converts `*.prof` files obtained from profiling runs of
MAlonzo-compiled code to `*.agdaIdents.prof`, with the original Agda
identifiers replacing the MAlonzo-generated Haskell identifiers.
For usage and more details, see `src/agda-ghc-names/README.txt`.
Highlighting and textual backends
---------------------------------
* Names in import directives are now highlighted and are clickable.
[Issue [#1714](https://github.com/agda/agda/issues/1714)] This leads
also to nicer printing in the LaTeX and html backends.
Fixed issues
------------
See
[bug tracker (milestone 2.5.1)](https://github.com/agda/agda/issues?q=milestone%3A2.5.1+is%3Aclosed)