Release notes for Agda version 2.6.2

Installation and infrastructure

Added support for GHC 8.10.1 [Issue #4242] and GHC 8.8.3 [Issue #4476].

Command-line interaction

In the previous release, Agda exited with either status 0 when the program type checks successfully, or status 1 when encountering any kind of error. Now Agda exits with status 42 for type errors, 71 for errors in the commandline arguments, and 154 for impossible errors. Exit status 1 may be returned under other circumstances; for instance, an incomplete pattern matching, or an error generated by the Haskell runtime. See PR #4540.

Pragmas and options

New options --qualified-instances (default) and --no-qualified-instances. When --no-qualified-instances is enabled, Agda will only consider candidates for instance search that are in scope under an unqualified name (see #4522).
New option --call-by-name turns off call-by-need evaluation at type checking time.
New option --highlight-occurrences (off by default) enables the HTML backend to include a JavaScript file that highlights all occurrences of the mouse-hovered symbol (see #4535).
New option --no-import-sorts disables the implicit open import Agda.Primitive using (Set; Prop) at the top of each file (see below).
New option --auto-inline turns on automatic compile-time inlining of simple functions. This was previously enabled by default.

Language

Inductive records without η-equality no longer support both matching on the record constructor and construction of record elements by copattern matching. It has been discovered that the combination of both leads to loss of subject reduction, i.e., reduction does not preserve typing. See issue #4560.

η-equality for a record can be turned off manually with directive no-eta-equality or command-line option --no-eta-equality, but it is also automatically turned off for some recursive records. For records without η, matching on the record constructor is now off by default and construction by copattern matching is on. If you want the converse, you can add the new record directive pattern.

Example with record pattern:
```
record N : Set where
  inductive
  no-eta-equality
  pattern
  field out : Maybe N

pred : N → Maybe N
pred record{ out = m } = m
```
Example with record constructor and use of ; instead of newline:
```
record N : Set where
  inductive; no-eta-equality
  pattern; constructor inn
  field out : Maybe N

pred : N → Maybe N
pred (inn m) = m
```
Set and Prop are no longer keywords but are now primitives defined in the module Agda.Primitive. They can be renamed when importing this module, for example:
```
open import Agda.Primitive renaming (Set to Type)

test : Type₁
test = Type
```
To preserve backwards compatibility, each top-level Agda module now starts with an implicit statement:
```
open import Agda.Primitive using (Set; Prop)
```
This implicit import can be disabled with the --no-import-sorts flag.
Agda now has support for sorts Setωᵢ (alternative syntax: Setωi) for natural numbers i, where Setω₀ = Setω. These sorts form a second hierarchy Setωᵢ : Setωᵢ₊₁ similar to the standard hierarchy of Setᵢ, but do not support universe polymorphism. It should not be necessary to refer to these sorts during normal usage of Agda, but they might be useful for defining reflection-based macros (see #2119 and #4585).
Changed the internal representation of literal strings: instead of using a linked list of characters (String), we are now using Data.Text. This should be a transparent change from the user's point of view: the backend was already packing these strings as text.

Used this opportunity to introduce a primStringUncons primitive in Agda.Builtin.String (and to correspondingly add the Agda.Builtin.Maybe it needs).

Reflection

New operation in TC monad, similar to quoteTC but operating on types in Setω
```
quoteωTC : ∀ {A : Setω} → A → TC Term
```
typeError and debugPrint no longer inserts spaces around termErr and nameErr parts. They also do a better job of respecting line breaks in strErr parts.
The representation of reflected patterns and clauses has changed. Each clause now includes a telescope with the names and types of the pattern variables.
```
data Clause where
  clause        : (tel : List (Σ String λ _ → Arg Type)) (ps : List (Arg Pattern)) (t : Term) → Clause
  absurd-clause : (tel : List (Σ String λ _ → Arg Type)) (ps : List (Arg Pattern)) → Clause
```
These telescopes provide additional information on the types of pattern variables that was previously hard to reconstruct (see #2151). When unquoting a clause, the types in the clause telescope are currently ignored (but this is subject to change in the future).

Two constructors of the Pattern datatype were also changed: pattern variables now refer to a de Bruijn index (relative to the clause telescope) rather than a string, and dot patterns now include the actual dotted term.
```
data Pattern where
  con    : (c : Name) (ps : List (Arg Pattern)) → Pattern
  dot    : (t : Term)    → Pattern   -- previously:   dot : Pattern
  var    : (x : Nat)     → Pattern   -- previously:   var : (x : String) → Pattern
  lit    : (l : Literal) → Pattern
  proj   : (f : Name)    → Pattern
  absurd : Pattern
```
It is likely that this change to the reflected syntax requires you to update reflection code written for previous versions of Agda. Here are some tips for updating your code:
- When quoting a clause, you can recover the name of a pattern variable by looking up the given index in the clause telescope. The contents of dot patterns can safely be ignored (unless you have a use for them).
- When creating a new clause for unquoting, you need to create a telescope for the types of the pattern variables. To get back the old behaviour of Agda, it is sufficient to set all the types of the pattern variables to unknown. So you can construct the telescope by listing the names of all pattern variables together with their ArgInfo. Meanwhile, the pattern variables should be numbered in order to update them to the new representation. As for the telescope types, the contents of a dot pattern can safely be set to unknown.

Emacs mode

New command prefix C-u C-u C-u for weak-head normalization. For instance, given
```
downFrom : Nat → List Nat
downFrom 0 = []
downFrom (suc n) = n ∷ downFrom n
```
C-u C-u C-u C-c C-n downFrom 5 returns 4 ∷ downFrom 4.

JS backend

Smaller local variable names in the generated JS code.

Previously: x0, x1, x2, ...

Now: a, b, c, ..., z, a0, b0, ..., z0, a1, b1, ...
Improved indentation of generated JS code.

More compact rendering of generated JS functions.

Previously:

exports["N"]["suc"] = function (x0) {
    return function (x1) {
      return x1["suc"](x0);
    };
  };

Now:

exports["N"]["suc"] = a => b => b["suc"](a);

Irrelevant arguments are now erased in the generated JS code.

Example Agda code:

flip : {A B C : Set} -> (B -> A -> C) -> A -> B -> C
flip f a b = f b a

Previously generated JS code:

exports["flip"] = function (x0) {
    return function (x1) {
      return function (x2) {
        return function (x3) {
          return function (x4) {
            return function (x5) {
              return x3(x5)(x4);
            };
          };
        };
      };
    };
  };

JS code generated now:

exports["flip"] = a => b => c => a(c)(b);

Record fields are not stored separately (the fields are stored only in the constructor) in the generated JS code.

Example Agda code:

record Sigma (A : Set) (B : A -> Set) : Set where
  field
    fst : A
    snd : B fst

Previously generated JS code (look at the "fst" and "snd" fields in the return value of exports["Sigma"]["record"]:

exports["Sigma"] = {};
exports["Sigma"]["fst"] = function (x0) {
    return x0["record"]({
      "record": function (x1, x2) {
        return x1;
      }
    });
  };
exports["Sigma"]["snd"] = function (x0) {
    return x0["record"]({
      "record": function (x1, x2) {
        return x2;
      }
    });
  };
exports["Sigma"]["record"] = function (x0) {
    return function (x1) {
      return {
        "fst": x0,
        "record": function (x2) {
          return x2["record"](x0, x1);
        },
        "snd": x1
      };
    };
  };

JS code generated now:

exports["Sigma"] = {};
exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b});
exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c});
exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});

--js-optimize flag has been added to the agda compiler.

With --js-optimize, agda does not wrap records in JS objects.

Example Agda code:

record Sigma (A : Set) (B : A -> Set) : Set where
  field
    fst : A
    snd : B fst

JS code generated without the --js-optimize flag:

exports["Sigma"] = {};
exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b});
exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c});
exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});

JS code generated with the --js-optimize flag:

exports["Sigma"] = {};
exports["Sigma"]["fst"] = a => a((b,c) => b);
exports["Sigma"]["snd"] = a => a((b,c) => c);
exports["Sigma"]["record"] = a => b => c => c(a,b);

With --js-optimize, agda uses JS arrays instead of JS objects. This is possible because constructor names are not relevant during the evaluation.

Example Agda code:

data Bool : Set where
  false : Bool
  true  : Bool

not : Bool -> Bool
not false = true
not true  = false

JS code generated without the --js-optimize flag:

exports["Bool"] = {};
exports["Bool"]["false"] = a => a["false"]();
exports["Bool"]["true"] = a => a["true"]();
exports["not"] = a => a({
    "false": () => exports["Bool"]["true"],
    "true": () => exports["Bool"]["false"]
  });

JS code generated with the --js-optimize flag:

exports["Bool"] = {};
exports["Bool"]["false"] = a => a[0/* false */]();
exports["Bool"]["true"] = a => a[1/* true */]();
exports["not"] = a => a([
    /* false */() => exports["Bool"]["true"],
    /* true */() => exports["Bool"]["false"]
  ]);

Note that comments are added to generated JS code to help human readers.

Erased branches are replaced by null in the generated array. If more than the half of branches are erased, the array is compressed to be a object like {3: ..., 13: ...}.

--js-minify flag has been added to the agda compiler.

With --js-minify, agda discards comments and whitespace in the generated JS code.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

CHANGELOG.md

CHANGELOG.md

Release notes for Agda version 2.6.2

Installation and infrastructure

Command-line interaction

Pragmas and options

Language

Reflection

Emacs mode

JS backend

Files

CHANGELOG.md

Latest commit

History

CHANGELOG.md

File metadata and controls

Release notes for Agda version 2.6.2

Installation and infrastructure

Command-line interaction

Pragmas and options

Language

Reflection

Emacs mode

JS backend