Release notes for Agda version 2.5.4

Installation and infrastructure

Added support for GHC 8.2.2 and GHC 8.4.3.

Note that GHC 8.4.* requires cabal-install ≥ 2.2.0.0.

Removed support for GHC 7.8.4.
Included user manual in PDF format in doc/user-manual.pdf.

Language

Call-by-need reduction.

Compile-time weak-head evaluation is now call-by-need, but each weak-head reduction has a local heap, so sharing is not maintained between different reductions.

The reduction machine has been rewritten from scratch and should be faster than the old one in all cases, even those not exploiting laziness.

Compile-time inlining.

Simple definitions (that don't do any pattern matching) marked as INLINE are now also inlined at compile time, whereas before they were only inlined by the compiler backends. Inlining only triggers in function bodies and not in type signatures, to preserve goal types as far as possible.

Automatic inlining.

Definitions satisfying the following criteria are now automatically inlined (can be disabled using the new NOINLINE pragma):

- No pattern matching.
- Uses each argument at most once.
- Does not use all its arguments.

Automatic inlining can be turned off using the flag --no-auto-inline. This can be useful when debugging tactics that may be affected by whether or not a particular definition is being inlined.

Syntax

Do-notation.

There is now builtin do-notation syntax. This means that do is a reserved keyword and cannot be used as an identifier.

Do-blocks support lets and pattern matching binds. If the pattern in a bind is non-exhaustive the other patterns need to be handled in a where-clause (see example below).

Example:

  filter : {A : Set} → (A → Bool) → List A → List A
  filter p xs = do
    x    ← xs
    true ← return (p x)
      where false → []
    return x

Do-blocks desugar to _>>=_ and _>>_ before scope checking, so whatever definitions of these two functions are in scope of the do-block will be used.

More precisely:

Simple bind
```
do x ← m
   m'
```
desugars to m >>= λ x → m'.
Pattern bind
```
do p ← m where pᵢ → mᵢ
   m'
```
desugars to m >>= λ { p → m'; pᵢ → mᵢ }, where pᵢ → mᵢ is an arbitrary sequence of clauses and follows the usual layout rules for where. If p is exhaustive the where clause can be omitted.
Non-binding operation
```
do m
   m'
```
desugars to m >> m'.
Let
```
do let ds
   m
```
desugars to let ds in m, where ds is an arbitrary sequence of valid let-declarations.
The last statement in the do block must be a plain expression (no let or bind).

Bind statements can use either ← or <-. Neither of these are reserved, so code outside do-blocks can use identifiers with these names, but inside a do-block they would need to be used qualified or under different names.

Infix let declarations. [Issue #917]

Let declarations can now be defined in infix (or mixfix) style. For instance:

    f : Nat → Nat
    f n = let _!_ : Nat → Nat → Nat
              x ! y = 2 * x + y
          in n ! n

Overloaded pattern synonyms. [Issue #2787]

Pattern synonyms can now be overloaded if all candidates have the same shape. Two pattern synonym definitions have the same shape if they are equal up to variable and constructor names. Shapes are checked at resolution time.

For instance, the following is accepted:

    open import Agda.Builtin.Nat

    data List (A : Set) : Set where
      lnil  : List A
      lcons : A → List A → List A

    data Vec (A : Set) : Nat → Set where
      vnil  : Vec A 0
      vcons : ∀ {n} → A → Vec A n → Vec A (suc n)

    pattern [] = lnil
    pattern [] = vnil

    pattern _∷_ x xs = lcons x xs
    pattern _∷_ y ys = vcons y ys

    lmap : ∀ {A B} → (A → B) → List A → List B
    lmap f []       = []
    lmap f (x ∷ xs) = f x ∷ lmap f xs

    vmap : ∀ {A B n} → (A → B) → Vec A n → Vec B n
    vmap f []       = []
    vmap f (x ∷ xs) = f x ∷ vmap f xs

If the file has no top-level module header, the first module cannot have the same name as the file. [Issues #2808 and #1077]

This means that the following file File.agda is rejected:

    -- no module header
    postulate A : Set
    module File where -- inner module with the same name as the file

Agda reports Illegal declarations(s) before top-level module at the postulate. This is to avoid confusing scope errors in similar situations.

If a top-level module header is inserted manually, the file is accepted:

    module _ where    -- user written module header
    postulate A : Set
    module File where -- inner module with the same name as the file, ok

Pattern matching

Forced constructor patterns.

Constructor patterns can now be dotted to indicate that Agda should not case split on them but rather their value is forced by the type of the other patterns. The difference between this and a regular dot pattern is that forced constructor patterns can still bind variables in their arguments. For example,

    open import Agda.Builtin.Nat

    data Vec (A : Set) : Nat → Set where
      nil  : Vec A zero
      cons : (n : Nat) → A → Vec A n → Vec A (suc n)

    append : {A : Set} (m n : Nat) → Vec A m → Vec A n → Vec A (m + n)
    append .zero    n nil            ys = ys
    append (.suc m) n (cons .m x xs) ys = cons (m + n) x (append m n xs ys)

Inferring the type of a function based on its patterns

Agda no longer infers the type of a function based on the patterns used in its definition. [Issue #2834]

This means that the following Agda program is no longer accepted:

    open import Agda.Builtin.Nat

    f : _ → _
    f zero    = zero
    f (suc n) = n

Agda now requires the type of the argument of f to be given explicitly.

Improved constraint solving for pattern matching functions

Constraint solving for functions where each right-hand side has a distinct rigid head has been extended to also cover the case where some clauses return an argument of the function. A typical example is append on lists:

    _++_ : {A : Set} → List A → List A → List A
    []       ++ ys = ys
    (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

Agda can now solve constraints like ?X ++ ys == 1 ∷ ys when ys is a neutral term.

Record expressions translated to copatterns

Definitions of the form

    f ps = record { f₁ = e₁; ..; fₙ = eₙ }

are translated internally to use copatterns:

    f ps .f₁ = e₁
    ...
    f ps .fₙ = eₙ

This means that f ps does not reduce, but thanks to η-equality the two definitions are equivalent.

The change should lead to fewer big record expressions showing up in goal types, and potentially significant performance improvement in some cases.

This may have a minor impact on with-abstraction and code using --rewriting since η-equality is not used in these cases.

When using with, it is now allowed to replace any pattern from the parent clause by a variable in the with clause. For example:

    f : List ℕ → List ℕ
    f [] = []
    f (x ∷ xs) with x ≤? 10
    f xs | p = {!!}

In the with clause, xs is treated as a let-bound variable with value .x ∷ .xs (where .x : ℕ and .xs : List ℕ are out of scope) and p : Dec (.x ≤ 10).

Since with-abstraction may change the type of variables, instantiations of variables in the with clause are type checked again after with-abstraction.

Builtins

Added support for built-in 64-bit machine words.

These are defined in Agda.Builtin.Word and come with two primitive operations to convert to and from natural numbers.

    Word64 : Set
    primWord64ToNat   : Word64 → Nat
    primWord64FromNat : Nat → Word64

Converting to a natural number is the trivial embedding, and converting from a natural number gives you the remainder modulo 2^64. The proofs of these theorems are not primitive, but can be defined in a library using primTrustMe.

Basic arithmetic operations can be defined on Word64 by converting to natural numbers, peforming the corresponding operation, and then converting back. The compiler will optimise these to use 64-bit arithmetic. For instance,

    addWord : Word64 → Word64 → Word64
    addWord a b = primWord64FromNat (primWord64ToNat a + primWord64ToNat b)

    subWord : Word64 → Word64 → Word64
    subWord a b = primWord64FromNat (primWord64ToNat a + 18446744073709551616 - primWord64ToNat b)

These compiles (in the GHC backend) to addition and subtraction on Data.Word.Word64.

New primitive primFloatLess and changed semantics of primFloatNumericalLess.

primFloatNumericalLess now uses standard IEEE <, so for instance NaN < x = x < NaN = false.

On the other hand primFloatLess provides a total order on Float, with -Inf < NaN < -1.0 < -0.0 < 0.0 < 1.0 < Inf.

The SIZEINF builtin is now given the name ∞ in Agda.Builtin.Size [Issue #2931].

Previously it was given the name ω.

Reflection

New TC primitive: declarePostulate. [Issue #2782]

    declarePostulate : Arg Name → Type → TC ⊤

This can be used to declare new postulates. The Visibility of the Arg must not be hidden. This feature fails when executed with --safe flag from command-line.

Pragmas and options

The --caching option is ON by default and is also a valid pragma. Caching can (sometimes) speed up re-typechecking in --interaction mode by reusing the result of the previous typechecking for the prefix of the file that has not changed (with a granularity at the level of declarations/mutual blocks).

It can be turned off by passing --no-caching to agda or with the following at the top of your file.

    {-# OPTIONS --no-caching #-}

The --sharing and --no-sharing options have been deprecated and do nothing.

Compile-time evaluation is now always call-by-need.

BUILTIN pragmas can now appear before the top-level module header and in parametrized modules. [Issue #2824]

{-# OPTIONS --rewriting #-}
open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}  -- here
module TopLevel (A : Set) where
{-# BUILTIN REWRITE _≡_ #-}  -- or here

Note that it is still the case that built-ins cannot be bound if they depend on module parameters from an enclosing module. For instance, the following is illegal:

module _ {a} {A : Set a} where
  data _≡_ (x : A) : A → Set a where
    refl : x ≡ x
  {-# BUILTIN EQUALITY _≡_ #-}

Builtin NIL and CONS have been merged with LIST.

When binding the LIST builtin, NIL and CONS are bound to the appropriate constructors automatically. This means that instead of writing

  {-# BUILTIN LIST List #-}
  {-# BUILTIN NIL  []   #-}
  {-# BUILTIN CONS _∷_  #-}

you just write

  {-# BUILTIN LIST List #-}

Attempting to bind NIL or CONS results in a warning and has otherwise no effect.

The --no-unicode pragma prevents Agda from introducing unicode characters when pretty printing a term. Lambda, Arrows and Forall quantifiers are all replaced by their ascii only version. Instead of resorting to subscript suffixes, Agda uses ascii digit characters.
New option --inversion-max-depth=N.

The depth is used to avoid looping due to inverting pattern matching for unsatisfiable constraints [Issue #431]. This option is only expected to be necessary in pathological cases.

New option --no-print-pattern-synonyms.

This disables the use of pattern synonyms in output from Agda. See [Issue #2902] for situations where this might be desirable.

New fine-grained control over the warning machinery: ability to (en/dis)able warnings on a one-by-one basis.
The command line option --help now takes an optional argument which allows the user to request more specific usage information about particular topics. The only one added so far is warning.
New pragma NOINLINE.

  {-# NOINLINE f #-}

Disables automatic inlining of f.

New pragma WARNING_ON_USAGE

  {-# WARNING_ON_USAGE QName Message #}

Prints Message whenever QName is used.

Emacs mode

Banana brackets have been added to the Agda input method.

\((   #x2985  LEFT  WHITE PARENTHESIS
\))   #x2986  RIGHT WHITE PARENTHESIS

Result splitting will introduce the trailing hidden arguments, if there is nothing else todo [Issue #2871]. Example: ```agda data Fun (A : Set) : Set where mkFun : (A → A) → Fun A

test : {A : Set} → Fun A test = ?

  Splitting on the result here (`C-c C-c RET`) will append
  `{A}` to the left hand side.
  ```agda
    test {A} = ?

Light highlighting is performed dynamically, even if the file is not loaded [Issue #2794].

This light highlighting is based on the token stream generated by Agda's lexer: the code is only highlighted if the file is lexically correct. If the Agda backend is not busy with something else, then the code is highlighted automatically in certain situations:

When the file is saved.
When Emacs has been idle, continuously, for a certain period of time (by default 0.2 s) after the last modification of the file, and the file has not been saved (or marked as being unmodified). This functionality can be turned off, and the time period can be customised.
Highlighting of comments is no longer handled by Font Lock mode [Issue #2794].
The Emacs mode's syntax table has been changed.

Previously _ was treated as punctuation. Now it is treated in the same way as most other characters: if the standard syntax table assigns it the syntax class "whitespace", "open parenthesis" or "close parenthesis", then it gets that syntax class, and otherwise it gets the syntax class "word constituent".

Compiler backends

The GHC backend now automatically compiles BUILTIN LIST to Haskell lists.

This means that it's no longer necessary to give a COMPILE GHC pragma for the builtin list type. Indeed, doing so has no effect on the compilation and results in a warning.

The GHC backend performance improvements.

Generated Haskell code now contains approximate type signatures, which lets GHC get rid of many of the unsafeCoerces. This leads to performance improvements of up to 50% of compiled code.

The GHC backend now compiles the INFINITY, SHARP and FLAT builtins in a different way [Issue #2909].

Previously these were compiled to (basically) nothing. Now the INFINITY builtin is compiled to Infinity, available from MAlonzo.RTE:

  data Inf a            = Sharp { flat :: a }
  type Infinity level a = Inf a

The SHARP builtin is compiled to Sharp, and the FLAT builtin is (by default) compiled to a corresponding destructor.

Note that code that interacts with Haskell libraries may have to be updated. As an example, here is one way to print colists of characters using the Haskell function putStr:

  open import Agda.Builtin.Char
  open import Agda.Builtin.Coinduction
  open import Agda.Builtin.IO
  open import Agda.Builtin.Unit

  data Colist {a} (A : Set a) : Set a where
    []  : Colist A
    _∷_ : A → ∞ (Colist A) → Colist A

  {-# FOREIGN GHC
    data Colist a    = Nil | Cons a (MAlonzo.RTE.Inf (Colist a))
    type Colist' l a = Colist a

    fromColist :: Colist a -> [a]
    fromColist Nil         = []
    fromColist (Cons x xs) = x : fromColist (MAlonzo.RTE.flat xs)
    #-}

  {-# COMPILE GHC Colist = data Colist' (Nil | Cons) #-}

  postulate
    putStr : Colist Char → IO ⊤

  {-# COMPILE GHC putStr = putStr . fromColist #-}

COMPILE GHC pragmas have been included for the size primitives [Issue #2879].

LaTeX backend

The code environment can now take arguments [Issues #2744 and #2453].

Everything from \begin{code} to the end of the line is preserved in the generated LaTeX code, and not treated as Agda code.

The default implementation of the code environment recognises one optional argument, hide, which can be used for code that should be type-checked, but not typeset:

  \begin{code}[hide]
    open import Module
  \end{code}

The AgdaHide macro has not been removed, but has been deprecated in favour of [hide].

The AgdaSuppressSpace and AgdaMultiCode environments no longer take an argument.

Instead some documents need to be compiled multiple times.

The --count-clusters flag can now be given in OPTIONS pragmas.
The nofontsetup option to the LaTeX package agda was broken, and has (hopefully) been fixed [Issue #2773].

Fewer packages than before are loaded when nofontsetup is used, see agda.sty for details. Furthermore, if LuaLaTeX or XeLaTeX are not used, then the font encoding is no longer changed.

The new option noinputencodingsetup instructs the LaTeX package agda to not change the input encoding, and to not load the ucs package.
Underscores are now typeset using \AgdaUnderscore{}.

The default implementation is \_ (the command that was previously generated for underscores). Note that it is possible to override this implementation.

OtherAspects (unsolved meta variables, catchall clauses, etc.) are now correctly highlighted in the LaTeX backend (and the HTML one). [Issue #2474]
postprocess-latex.pl does not add extra spaces around tagged \Agda*{} commands anymore.

HTML backend

An identifier (excluding bound variables), gets the identifier itself as an anchor, in addition to the file position [Issue #2756]. In Agda 2.5.3, the identifier anchor would replace the file position anchor [Issue #2604].

Symbolic anchors look like

  <a id="test1">
  <a id="M.bla">

while file position anchors just give the character position in the file:

  <a id="42">

Top-level module names do not get a symbolic anchor, since the position of a top-level module is defined to be the beginning of the file.