Release notes for Agda 2 version 2.3.0
======================================
Language
--------
* New more liberal syntax for mutually recursive definitions.
It is no longer necessary to use the `mutual` keyword to define
mutually recursive functions or datatypes. Instead, it is enough to
declare things before they are used. Instead of
```agda
mutual
f : A
f = a[f, g]
g : B[f]
g = b[f, g]
```
you can now write
```agda
f : A
g : B[f]
f = a[f, g]
g = b[f, g].
```
With the new style you have more freedom in choosing the order in
which things are type checked (previously type signatures were
always checked before definitions). Furthermore you can mix
arbitrary declarations, such as modules and postulates, with
mutually recursive definitions.
For data types and records the following new syntax is used to
separate the declaration from the definition:
```agda
-- Declaration.
data Vec (A : Set) : Nat → Set -- Note the absence of 'where'.
-- Definition.
data Vec A where
[] : Vec A zero
_::_ : {n : Nat} → A → Vec A n → Vec A (suc n)
-- Declaration.
record Sigma (A : Set) (B : A → Set) : Set
-- Definition.
record Sigma A B where
constructor _,_
field fst : A
snd : B fst
```
When making separated declarations/definitions private or abstract
you should attach the `private` keyword to the declaration and the
`abstract` keyword to the definition. For instance, a private,
abstract function can be defined as
```agda
private
f : A
abstract
f = e
```
Finally it may be worth noting that the old style of mutually
recursive definitions is still supported (it basically desugars into
the new style).
* Pattern matching lambdas.
Anonymous pattern matching functions can be defined using the syntax
```
\ { p11 .. p1n -> e1 ; ... ; pm1 .. pmn -> em }
```
(where, as usual, `\` and `->` can be replaced by `λ` and
`→`). Internally this is translated into a function definition of
the following form:
```
.extlam p11 .. p1n = e1
...
.extlam pm1 .. pmn = em
```
This means that anonymous pattern matching functions are generative.
For instance, `refl` will not be accepted as an inhabitant of the type
```agda
(λ { true → true ; false → false }) ≡
(λ { true → true ; false → false }),
```
because this is equivalent to `extlam1 ≡ extlam2` for some distinct
fresh names `extlam1` and `extlam2`.
Currently the `where` and `with` constructions are not allowed in
(the top-level clauses of) anonymous pattern matching functions.
Examples:
```agda
and : Bool → Bool → Bool
and = λ { true x → x ; false _ → false }
xor : Bool → Bool → Bool
xor = λ { true true → false
; false false → false
; _ _ → true
}
fst : {A : Set} {B : A → Set} → Σ A B → A
fst = λ { (a , b) → a }
snd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p)
snd = λ { (a , b) → b }
```
* Record update syntax.
Assume that we have a record type and a corresponding value:
```agda
record MyRecord : Set where
field
a b c : ℕ
old : MyRecord
old = record { a = 1; b = 2; c = 3 }
```
Then we can update (some of) the record value's fields in the
following way:
```agda
new : MyRecord
new = record old { a = 0; c = 5 }
```
Here new normalises to `record { a = 0; b = 2; c = 5 }`. Any
expression yielding a value of type `MyRecord` can be used instead of
old.
Record updating is not allowed to change types: the resulting value
must have the same type as the original one, including the record
parameters. Thus, the type of a record update can be inferred if the
type of the original record can be inferred.
The record update syntax is expanded before type checking. When the
expression
```agda
record old { upd-fields }
```
is checked against a record type `R`, it is expanded to
```agda
let r = old in record { new-fields },
```
where old is required to have type `R` and new-fields is defined as
follows: for each field `x` in `R`,
- if `x = e` is contained in `upd-fields` then `x = e` is included in
`new-fields`, and otherwise
- if `x` is an explicit field then `x = R.x r` is included in
`new-fields`, and
- if `x` is an implicit or instance field, then it is omitted from
`new-fields`.
(Instance arguments are explained below.) The reason for treating
implicit and instance fields specially is to allow code like the
following:
```agda
record R : Set where
field
{length} : ℕ
vec : Vec ℕ length
-- More fields…
xs : R
xs = record { vec = 0 ∷ 1 ∷ 2 ∷ [] }
ys = record xs { vec = 0 ∷ [] }
```
Without the special treatment the last expression would need to
include a new binding for length (for instance `length = _`).
* Record patterns which do not contain data type patterns, but which
do contain dot patterns, are no longer rejected.
* When the `--without-K` flag is used literals are now treated as
constructors.
* Under-applied functions can now reduce.
Consider the following definition:
```agda
id : {A : Set} → A → A
id x = x
```
Previously the expression `id` would not reduce. This has been
changed so that it now reduces to `λ x → x`. Usually this makes
little difference, but it can be important in conjunction with
`with`. See Issue [#365](https://github.com/agda/agda/issues/365)
for an example.
* Unused AgdaLight legacy syntax `(x y : A; z v : B)` for telescopes
has been removed.
### Universe polymorphism
* Universe polymorphism is now enabled by default. Use
`--no-universe-polymorphism` to disable it.
* Universe levels are no longer defined as a data type.
The basic level combinators can be introduced in the following way:
```agda
postulate
Level : Set
zero : Level
suc : Level → Level
max : Level → Level → Level
{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO zero #-}
{-# BUILTIN LEVELSUC suc #-}
{-# BUILTIN LEVELMAX max #-}
```
* The BUILTIN equality is now required to be universe-polymorphic.
* `trustMe` is now universe-polymorphic.
### Meta-variables and unification
* Unsolved meta-variables are now frozen after every mutual block.
This means that they cannot be instantiated by subsequent code. For
instance,
```agda
one : Nat
one = _
bla : one ≡ suc zero
bla = refl
```
leads to an error now, whereas previously it lead to the
instantiation of `_` with `suc zero`. If you want to make use of the
old behaviour, put the two definitions in a mutual block.
All meta-variables are unfrozen during interactive editing, so that
the user can fill holes interactively. Note that type-checking of
interactively given terms is not perfect: Agda sometimes refuses to
load a file, even though no complaints were raised during the
interactive construction of the file. This is because certain checks
(for instance, positivity) are only invoked when a file is loaded.
* Record types can now be inferred.
If there is a unique known record type with fields matching the
fields in a record expression, then the type of the expression will
be inferred to be the record type applied to unknown parameters.
If there is no known record type with the given fields the type
checker will give an error instead of producing lots of unsolved
meta-variables.
Note that "known record type" refers to any record type in any
imported module, not just types which are in scope.
* The occurrence checker distinguishes rigid and strongly rigid
occurrences [Reed, LFMTP 2009; Abel & Pientka, TLCA 2011].
The completeness checker now accepts the following code:
```agda
h : (n : Nat) → n ≡ suc n → Nat
h n ()
```
Internally this generates a constraint `_n = suc _n` where the
meta-variable `_n` occurs strongly rigidly, i.e. on a constructor
path from the root, in its own defining term tree. This is never
solvable.
Weakly rigid recursive occurrences may have a solution [Jason Reed's
PhD thesis, page 106]:
```agda
test : (k : Nat) →
let X : (Nat → Nat) → Nat
X = _
in
(f : Nat → Nat) → X f ≡ suc (f (X (λ x → k)))
test k f = refl
```
The constraint `_X k f = suc (f (_X k (λ x → k)))` has the solution
`_X k f = suc (f (suc k))`, despite the recursive occurrence of
`_X`. Here `_X` is not strongly rigid, because it occurs under the
bound variable `f`. Previously Agda rejected this code; now it instead
complains about an unsolved meta-variable.
* Equation constraints involving the same meta-variable in the head
now trigger pruning [Pientka, PhD, Sec. 3.1.2; Abel & Pientka, TLCA
2011]. Example:
```agda
same : let X : A → A → A → A × A
X = _
in {x y z : A} → X x y y ≡ (x , y)
× X x x y ≡ X x y y
same = refl , refl
```
The second equation implies that `X` cannot depend on its second
argument. After pruning the first equation is linear and can be
solved.
* Instance arguments.
A new type of hidden function arguments has been added: instance
arguments. This new feature is based on influences from Scala's
implicits and Agda's existing implicit arguments.
Plain implicit arguments are marked by single braces: `{…}`. Instance
arguments are instead marked by double braces: `{{…}}`. Example:
```agda
postulate
A : Set
B : A → Set
a : A
f : {{a : A}} → B a
```
Instead of the double braces you can use the symbols `⦃` and `⦄`,
but these symbols must in many cases be surrounded by
whitespace. (If you are using Emacs and the Agda input method, then
you can conjure up the symbols by typing `\{{` and `\}}`,
respectively.)
Instance arguments behave as ordinary implicit arguments, except for
one important aspect: resolution of arguments which are not provided
explicitly. For instance, consider the following code:
```agda
test = f
```
Here Agda will notice that `f`'s instance argument was not provided
explicitly, and try to infer it. All definitions in scope at `f`'s
call site, as well as all variables in the context, are considered.
If exactly one of these names has the required type `A`, then the
instance argument will be instantiated to this name.
This feature can be used as an alternative to Haskell type classes.
If we define
```agda
record Eq (A : Set) : Set where
field equal : A → A → Bool,
```
then we can define the following projection:
```agda
equal : {A : Set} {{eq : Eq A}} → A → A → Bool
equal {{eq}} = Eq.equal eq
```
Now consider the following expression:
```agda
equal false false ∨ equal 3 4
```
If the following `Eq` "instances" for `Bool` and `ℕ` are in scope, and no
others, then the expression is accepted:
```agda
eq-Bool : Eq Bool
eq-Bool = record { equal = … }
eq-ℕ : Eq ℕ
eq-ℕ = record { equal = … }
```
A shorthand notation is provided to avoid the need to define
projection functions manually:
```agda
module Eq-with-implicits = Eq {{...}}
```
This notation creates a variant of `Eq`'s record module, where the
main `Eq` argument is an instance argument instead of an explicit one.
It is equivalent to the following definition:
```agda
module Eq-with-implicits {A : Set} {{eq : Eq A}} = Eq eq
```
Note that the short-hand notation allows you to avoid naming the
"-with-implicits" module:
```agda
open Eq {{...}}
```
Instance argument resolution is not recursive. As an example,
consider the following "parametrised instance":
```agda
eq-List : {A : Set} → Eq A → Eq (List A)
eq-List {A} eq = record { equal = eq-List-A }
where
eq-List-A : List A → List A → Bool
eq-List-A [] [] = true
eq-List-A (a ∷ as) (b ∷ bs) = equal a b ∧ eq-List-A as bs
eq-List-A _ _ = false
```
Assume that the only `Eq` instances in scope are `eq-List` and
`eq-ℕ`. Then the following code does not type-check:
```agda
test = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])
```
However, we can make the code work by constructing a suitable
instance manually:
```agda
test′ = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])
where eq-List-ℕ = eq-List eq-ℕ
```
By restricting the "instance search" to be non-recursive we avoid
introducing a new, compile-time-only evaluation model to Agda.
For more information about instance arguments, see Devriese &
Piessens [ICFP 2011]. Some examples are also available in the
examples/instance-arguments subdirectory of the Agda distribution.
### Irrelevance
* Dependent irrelevant function types.
Some examples illustrating the syntax of dependent irrelevant
function types:
```
.(x y : A) → B .{x y z : A} → B
∀ x .y → B ∀ x .{y} {z} .v → B
```
The declaration
```
f : .(x : A) → B[x]
f x = t[x]
```
requires that `x` is irrelevant both in `t[x]` and in `B[x]`. This
is possible if, for instance, `B[x] = B′ x`, with `B′ : .A → Set`.
Dependent irrelevance allows us to define the eliminator for the
`Squash` type:
```agda
record Squash (A : Set) : Set where
constructor squash
field
.proof : A
elim-Squash : {A : Set} (P : Squash A → Set)
(ih : .(a : A) → P (squash a)) →
(a⁻ : Squash A) → P a⁻
elim-Squash P ih (squash a) = ih a
```
Note that this would not type-check with
```agda
(ih : (a : A) -> P (squash a)).
```
* Records with only irrelevant fields.
The following now works:
```agda
record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set where
field
.refl : Reflexive _≈_
.sym : Symmetric _≈_
.trans : Transitive _≈_
record Setoid : Set₁ where
infix 4 _≈_
field
Carrier : Set
_≈_ : Carrier → Carrier → Set
.isEquivalence : IsEquivalence _≈_
open IsEquivalence isEquivalence public
```
Previously Agda complained about the application
`IsEquivalence isEquivalence`, because `isEquivalence` is irrelevant
and the `IsEquivalence` module expected a relevant argument. Now,
when record modules are generated for records consisting solely of
irrelevant arguments, the record parameter is made irrelevant:
```agda
module IsEquivalence {A : Set} {_≈_ : A → A → Set}
.(r : IsEquivalence {A = A} _≈_) where
…
```
* Irrelevant things are no longer erased internally. This means that
they are printed as ordinary terms, not as `_` as before.
* The new flag `--experimental-irrelevance` enables irrelevant
universe levels and matching on irrelevant data when only one
constructor is available. These features are very experimental and
likely to change or disappear.
### Reflection
* The reflection API has been extended to mirror features like
irrelevance, instance arguments and universe polymorphism, and to
give (limited) access to definitions. For completeness all the
builtins and primitives are listed below:
```agda
-- Names.
postulate Name : Set
{-# BUILTIN QNAME Name #-}
primitive
-- Equality of names.
primQNameEquality : Name → Name → Bool
-- Is the argument visible (explicit), hidden (implicit), or an
-- instance argument?
data Visibility : Set where
visible hidden instance : Visibility
{-# BUILTIN HIDING Visibility #-}
{-# BUILTIN VISIBLE visible #-}
{-# BUILTIN HIDDEN hidden #-}
{-# BUILTIN INSTANCE instance #-}
-- Arguments can be relevant or irrelevant.
data Relevance : Set where
relevant irrelevant : Relevance
{-# BUILTIN RELEVANCE Relevance #-}
{-# BUILTIN RELEVANT relevant #-}
{-# BUILTIN IRRELEVANT irrelevant #-}
-- Arguments.
data Arg A : Set where
arg : (v : Visibility) (r : Relevance) (x : A) → Arg A
{-# BUILTIN ARG Arg #-}
{-# BUILTIN ARGARG arg #-}
-- Terms.
mutual
data Term : Set where
-- Variable applied to arguments.
var : (x : ℕ) (args : List (Arg Term)) → Term
-- Constructor applied to arguments.
con : (c : Name) (args : List (Arg Term)) → Term
-- Identifier applied to arguments.
def : (f : Name) (args : List (Arg Term)) → Term
-- Different kinds of λ-abstraction.
lam : (v : Visibility) (t : Term) → Term
-- Pi-type.
pi : (t₁ : Arg Type) (t₂ : Type) → Term
-- A sort.
sort : Sort → Term
-- Anything else.
unknown : Term
data Type : Set where
el : (s : Sort) (t : Term) → Type
data Sort : Set where
-- A Set of a given (possibly neutral) level.
set : (t : Term) → Sort
-- A Set of a given concrete level.
lit : (n : ℕ) → Sort
-- Anything else.
unknown : Sort
{-# BUILTIN AGDASORT Sort #-}
{-# BUILTIN AGDATYPE Type #-}
{-# BUILTIN AGDATERM Term #-}
{-# BUILTIN AGDATERMVAR var #-}
{-# BUILTIN AGDATERMCON con #-}
{-# BUILTIN AGDATERMDEF def #-}
{-# BUILTIN AGDATERMLAM lam #-}
{-# BUILTIN AGDATERMPI pi #-}
{-# BUILTIN AGDATERMSORT sort #-}
{-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
{-# BUILTIN AGDATYPEEL el #-}
{-# BUILTIN AGDASORTSET set #-}
{-# BUILTIN AGDASORTLIT lit #-}
{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}
postulate
-- Function definition.
Function : Set
-- Data type definition.
Data-type : Set
-- Record type definition.
Record : Set
{-# BUILTIN AGDAFUNDEF Function #-}
{-# BUILTIN AGDADATADEF Data-type #-}
{-# BUILTIN AGDARECORDDEF Record #-}
-- Definitions.
data Definition : Set where
function : Function → Definition
data-type : Data-type → Definition
record′ : Record → Definition
constructor′ : Definition
axiom : Definition
primitive′ : Definition
{-# BUILTIN AGDADEFINITION Definition #-}
{-# BUILTIN AGDADEFINITIONFUNDEF function #-}
{-# BUILTIN AGDADEFINITIONDATADEF data-type #-}
{-# BUILTIN AGDADEFINITIONRECORDDEF record′ #-}
{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR constructor′ #-}
{-# BUILTIN AGDADEFINITIONPOSTULATE axiom #-}
{-# BUILTIN AGDADEFINITIONPRIMITIVE primitive′ #-}
primitive
-- The type of the thing with the given name.
primQNameType : Name → Type
-- The definition of the thing with the given name.
primQNameDefinition : Name → Definition
-- The constructors of the given data type.
primDataConstructors : Data-type → List Name
```
As an example the expression
```agda
primQNameType (quote zero)
```
is definitionally equal to
```agda
el (lit 0) (def (quote ℕ) [])
```
(if `zero` is a constructor of the data type `ℕ`).
* New keyword: `unquote`.
The construction `unquote t` converts a representation of an Agda term
to actual Agda code in the following way:
1. The argument `t` must have type `Term` (see the reflection API above).
2. The argument is normalised.
3. The entire construction is replaced by the normal form, which is
treated as syntax written by the user and type-checked in the
usual way.
Examples:
```agda
test : unquote (def (quote ℕ) []) ≡ ℕ
test = refl
id : (A : Set) → A → A
id = unquote (lam visible (lam visible (var 0 [])))
id-ok : id ≡ (λ A (x : A) → x)
id-ok = refl
```
* New keyword: `quoteTerm`.
The construction `quoteTerm t` is similar to `quote n`, but whereas
`quote` is restricted to names `n`, `quoteTerm` accepts terms
`t`. The construction is handled in the following way:
1. The type of `t` is inferred. The term `t` must be type-correct.
2. The term `t` is normalised.
3. The construction is replaced by the Term representation (see the
reflection API above) of the normal form. Any unsolved metavariables
in the term are represented by the `unknown` term constructor.
Examples:
```agda
test₁ : quoteTerm (λ {A : Set} (x : A) → x) ≡
lam hidden (lam visible (var 0 []))
test₁ = refl
-- Local variables are represented as de Bruijn indices.
test₂ : (λ {A : Set} (x : A) → quoteTerm x) ≡ (λ x → var 0 [])
test₂ = refl
-- Terms are normalised before being quoted.
test₃ : quoteTerm (0 + 0) ≡ con (quote zero) []
test₃ = refl
```
Compiler backends
-----------------
### MAlonzo
* The MAlonzo backend's FFI now handles universe polymorphism in a
better way.
The translation of Agda types and kinds into Haskell now supports
universe-polymorphic postulates. The core changes are that the
translation of function types has been changed from
```
T[[ Pi (x : A) B ]] =
if A has a Haskell kind then
forall x. () -> T[[ B ]]
else if x in fv B then
undef
else
T[[ A ]] -> T[[ B ]]
```
into
```
T[[ Pi (x : A) B ]] =
if x in fv B then
forall x. T[[ A ]] -> T[[ B ]] -- Note: T[[A]] not Unit.
else
T[[ A ]] -> T[[ B ]],
```
and that the translation of constants (postulates, constructors and
literals) has been changed from
```
T[[ k As ]] =
if COMPILED_TYPE k T then
T T[[ As ]]
else
undef
```
into
```
T[[ k As ]] =
if COMPILED_TYPE k T then
T T[[ As ]]
else if COMPILED k E then
()
else
undef.
```
For instance, assuming a Haskell definition
```haskell
type AgdaIO a b = IO b,
```
we can set up universe-polymorphic `IO` in the following way:
```agda
postulate
IO : ∀ {ℓ} → Set ℓ → Set ℓ
return : ∀ {a} {A : Set a} → A → IO A
_>>=_ : ∀ {a b} {A : Set a} {B : Set b} →
IO A → (A → IO B) → IO B
{-# COMPILED_TYPE IO AgdaIO #-}
{-# COMPILED return (\_ _ -> return) #-}
{-# COMPILED _>>=_ (\_ _ _ _ -> (>>=)) #-}
```
This is accepted because (assuming that the universe level type is
translated to the Haskell unit type `()`)
```haskell
(\_ _ -> return)
: forall a. () -> forall b. () -> b -> AgdaIO a b
= T [[ ∀ {a} {A : Set a} → A → IO A ]]
```
and
```haskell
(\_ _ _ _ -> (>>=))
: forall a. () -> forall b. () ->
forall c. () -> forall d. () ->
AgdaIO a c -> (c -> AgdaIO b d) -> AgdaIO b d
= T [[ ∀ {a b} {A : Set a} {B : Set b} →
IO A → (A → IO B) → IO B ]].
```
### Epic
* New Epic backend pragma: `STATIC`.
In the Epic backend, functions marked with the `STATIC` pragma will be
normalised before compilation. Example usage:
```
{-# STATIC power #-}
power : ℕ → ℕ → ℕ
power 0 x = 1
power 1 x = x
power (suc n) x = power n x * x
```
Occurrences of `power 4 x` will be replaced by `((x * x) * x) * x`.
* Some new optimisations have been implemented in the Epic backend:
- Removal of unused arguments.
A worker/wrapper transformation is performed so that unused
arguments can be removed by Epic's inliner. For instance, the map
function is transformed in the following way:
```agda
map_wrap : (A B : Set) → (A → B) → List A → List B
map_wrap A B f xs = map_work f xs
map_work f [] = []
map_work f (x ∷ xs) = f x ∷ map_work f xs
```
If `map_wrap` is inlined (which it will be in any saturated call),
then `A` and `B` disappear in the generated code.
Unused arguments are found using abstract interpretation. The bodies
of all functions in a module are inspected to decide which variables
are used. The behaviour of postulates is approximated based on their
types. Consider `return`, for instance:
```agda
postulate return : {A : Set} → A → IO A
```
The first argument of `return` can be removed, because it is of type
Set and thus cannot affect the outcome of a program at runtime.
- Injection detection.
At runtime many functions may turn out to be inefficient variants of
the identity function. This is especially true after forcing.
Injection detection replaces some of these functions with more
efficient versions. Example:
```agda
inject : {n : ℕ} → Fin n → Fin (1 + n)
inject {suc n} zero = zero
inject {suc n} (suc i) = suc (inject {n} i)
```
Forcing removes the `Fin` constructors' `ℕ` arguments, so this
function is an inefficient identity function that can be replaced by
the following one:
```agda
inject {_} x = x
```
To actually find this function, we make the induction hypothesis
that inject is an identity function in its second argument and look
at the branches of the function to decide if this holds.
Injection detection also works over data type barriers. Example:
```agda
forget : {A : Set} {n : ℕ} → Vec A n → List A
forget [] = []
forget (x ∷ xs) = x ∷ forget xs
```
Given that the constructor tags (in the compiled Epic code) for
`Vec.[]` and `List.[]` are the same, and that the tags for `Vec._∷_`
and `List._∷_` are also the same, this is also an identity
function. We can hence replace the definition with the following
one:
```agda
forget {_} xs = xs
```
To get this to apply as often as possible, constructor tags are
chosen *after* injection detection has been run, in a way to make as
many functions as possible injections.
Constructor tags are chosen once per source file, so it may be
advantageous to define conversion functions like forget in the same
module as one of the data types. For instance, if `Vec.agda` imports
`List.agda`, then the forget function should be put in `Vec.agda` to
ensure that vectors and lists get the same tags (unless some other
injection function, which puts different constraints on the tags, is
prioritised).
- Smashing.
This optimisation finds types whose values are inferable at runtime:
* A data type with only one constructor where all fields are
inferable is itself inferable.
* `Set ℓ` is inferable (as it has no runtime representation).
A function returning an inferable data type can be smashed, which
means that it is replaced by a function which simply returns the
inferred value.
An important example of an inferable type is the usual propositional
equality type (`_≡_`). Any function returning a propositional
equality can simply return the reflexivity constructor directly
without computing anything.
This optimisation makes more arguments unused. It also makes the
Epic code size smaller, which in turn speeds up compilation.
### JavaScript
* ECMAScript compiler backend.
A new compiler backend is being implemented, targetting ECMAScript
(also known as JavaScript), with the goal of allowing Agda programs
to be run in browsers or other ECMAScript environments.
The backend is still at an experimental stage: the core language is
implemented, but many features are still missing.
The ECMAScript compiler can be invoked from the command line using
the flag `--js`:
```
agda --js --compile-dir=<DIR> <FILE>.agda
```
Each source `<FILE>.agda` is compiled into an ECMAScript target
`<DIR>/jAgda.<TOP-LEVEL MODULE NAME>.js`. The compiler can also be
invoked using the Emacs mode (the variable `agda2-backend` controls
which backend is used).
Note that ECMAScript is a strict rather than lazy language. Since
Agda programs are total, this should not impact program semantics,
but it may impact their space or time usage.
ECMAScript does not support algebraic datatypes or pattern-matching.
These features are translated to a use of the visitor pattern. For
instance, the standard library's `List` data type and `null`
function are translated into the following code:
```javascript
exports["List"] = {};
exports["List"]["[]"] = function (x0) {
return x0["[]"]();
};
exports["List"]["_∷_"] = function (x0) {
return function (x1) {
return function (x2) {
return x2["_∷_"](x0, x1);
};
};
};
exports["null"] = function (x0) {
return function (x1) {
return function (x2) {
return x2({
"[]": function () {
return jAgda_Data_Bool["Bool"]["true"];
},
"_∷_": function (x3, x4) {
return jAgda_Data_Bool["Bool"]["false"];
}
});
};
};
};
```
Agda records are translated to ECMAScript objects, preserving field
names.
Top-level Agda modules are translated to ECMAScript modules,
following the `common.js` module specification. A top-level Agda
module `Foo.Bar` is translated to an ECMAScript module
`jAgda.Foo.Bar`.
The ECMAScript compiler does not compile to Haskell, so the pragmas
related to the Haskell FFI (`IMPORT`, `COMPILED_DATA` and
`COMPILED`) are not used by the ECMAScript backend. Instead, there
is a `COMPILED_JS` pragma which may be applied to any
declaration. For postulates, primitives, functions and values, it
gives the ECMAScript code to be emitted by the compiler. For data
types, it gives a function which is applied to a value of that type,
and a visitor object. For instance, a binding of natural numbers to
ECMAScript integers (ignoring overflow errors) is:
```agda
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# COMPILED_JS ℕ function (x,v) {
if (x < 1) { return v.zero(); } else { return v.suc(x-1); }
} #-}
{-# COMPILED_JS zero 0 #-}
{-# COMPILED_JS suc function (x) { return x+1; } #-}
_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)
{-# COMPILED_JS _+_ function (x) { return function (y) {
return x+y; };
} #-}
```
To allow FFI code to be optimised, the ECMAScript in a `COMPILED_JS`
declaration is parsed, using a simple parser that recognises a pure
functional subset of ECMAScript, consisting of functions, function
applications, return, if-statements, if-expressions,
side-effect-free binary operators (no precedence, left associative),
side-effect-free prefix operators, objects (where all member names
are quoted), field accesses, and string and integer literals.
Modules may be imported using the require (`<module-id>`) syntax: any
impure code, or code outside the supported fragment, can be placed
in a module and imported.
Tools
-----
* New flag `--safe`, which can be used to type-check untrusted code.
This flag disables postulates, `primTrustMe`, and "unsafe" `OPTIONS`
pragmas, some of which are known to make Agda inconsistent.
Rejected pragmas:
```
--allow-unsolved-metas
--experimental-irrelevance
--guardedness-preserving-type-construtors
--injective-type-constructors
--no-coverage-check
--no-positivity-check
--no-termination-check
--sized-types
--type-in-type
```
Note that, at the moment, it is not possible to define the universe
level or coinduction primitives when `--safe` is used (because they
must be introduced as postulates). This can be worked around by
type-checking trusted files in a first pass, without using `--safe`,
and then using `--saf`e in a second pass. Modules which have already
been type-checked are not re-type-checked just because `--safe` is
used.
* Dependency graphs.
The new flag `--dependency-graph=FILE` can be used to generate a DOT
file containing a module dependency graph. The generated file (FILE)
can be rendered using a tool like dot.
* The `--no-unreachable-check` flag has been removed.
* Projection functions are highlighted as functions instead of as
fields. Field names (in record definitions and record values) are
still highlighted as fields.
* Support for jumping to positions mentioned in the information
buffer has been added.
* The `make install` command no longer installs Agda globally (by
default).