Release notes for Agda version 2.4.2.4

Installation and infrastructure

Removed support for GHC 7.4.2.

Pragmas and options

Option --copatterns is now on by default. To switch off parsing of copatterns, use:

  {-# OPTIONS --no-copatterns #-}

Option --rewriting is now needed to use REWRITE pragmas and rewriting during reduction. Rewriting is not --safe.

To use rewriting, first specify a relation symbol R that will later be used to add rewrite rules. A canonical candidate would be propositional equality

  {-# BUILTIN REWRITE _≡_ #-}

but any symbol R of type Δ → A → A → Set i for some A and i is accepted. Then symbols q can be added to rewriting provided their type is of the form Γ → R ds l r. This will add a rewrite rule

  Γ ⊢ l ↦ r : A[ds/Δ]

to the signature, which fires whenever a term is an instance of l. For example, if

  plus0 : ∀ x → x + 0 ≡ x

(ideally, there is a proof for plus0, but it could be a postulate), then

  {-# REWRITE plus0 #-}

will prompt Agda to rewrite any well-typed term of the form t + 0 to t.

Some caveats: Agda accepts and applies rewrite rules naively, it is very easy to break consistency and termination of type checking. Some examples of rewrite rules that should not be added:

  refl     : ∀ x → x ≡ x             -- Agda loops
  plus-sym : ∀ x y → x + y ≡ y + x   -- Agda loops
  absurd   : true ≡ false            -- Breaks consistency

Adding only proven equations should at least preserve consistency, but this is only a conjecture, so know what you are doing! Using rewriting, you are entering into the wilderness, where you are on your own!

Language

forall / ∀ now parses like λ, i.e., the following parses now [Issue #1583]:

  ⊤ × ∀ (B : Set) → B → B

The underscore pattern _ can now also stand for an inaccessible pattern (dot pattern). This alleviates the need for writing ._. [Issue #1605] Instead of

  transVOld : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
  transVOld _ ._ ._ refl refl = refl

one can now write

    transVNew : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
    transVNew _ _ _ refl refl = refl

and let Agda decide where to put the dots. This was always possible by using hidden arguments

  transH : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
  transH refl refl = refl

which is now equivalent to

  transHNew : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
  transHNew {a = _}{b = _}{c = _} refl refl = refl

Before, underscore _ stood for an unnamed variable that could not be instantiated by an inaccessible pattern. If one no wants to prevent Agda from instantiating, one needs to use a variable name other than underscore (however, in practice this situation seems unlikely).

Type checking

Polarity of phantom arguments to data and record types has changed. [Issue #1596] Polarity of size arguments is Nonvariant (both monotone and antitone). Polarity of other arguments is Covariant (monotone). Both were Invariant before (neither monotone nor antitone).

The following example type-checks now:

  open import Common.Size

  -- List should be monotone in both arguments
  -- (even when `cons' is missing).

  data List (i : Size) (A : Set) : Set where
    [] : List i A

  castLL : ∀{i A} → List i (List i A) → List ∞ (List ∞ A)
  castLL x = x

  -- Stream should be antitone in the first and monotone in the second argument
  -- (even with field `tail' missing).

  record Stream (i : Size) (A : Set) : Set where
    coinductive
    field
      head : A

  castSS : ∀{i A} → Stream ∞ (Stream ∞ A) → Stream i (Stream i A)
  castSS x = x

SIZELT lambdas must be consistent [Issue #1523, see Abel and Pientka, ICFP 2013]. When lambda-abstracting over type (Size< size) then size must be non-zero, for any valid instantiation of size variables.

The good:

data Nat (i : Size) : Set where
  zero : ∀ (j : Size< i) → Nat i
  suc  : ∀ (j : Size< i) → Nat j → Nat i

{-# TERMINATING #-}
-- This definition is fine, the termination checker is too strict at the moment.
fix : ∀ {C : Size → Set}
   → (∀ i → (∀ (j : Size< i) → Nat j -> C j) → Nat i → C i)
   → ∀ i → Nat i → C i
fix t i (zero j)  = t i (λ (k : Size< i) → fix t k) (zero j)
fix t i (suc j n) = t i (λ (k : Size< i) → fix t k) (suc j n)

The λ (k : Size< i) is fine in both cases, as context

i : Size, j : Size< i

guarantees that i is non-zero.

The bad:

record Stream {i : Size} (A : Set) : Set where
  coinductive
  constructor _∷ˢ_
  field
    head  : A
    tail  : ∀ {j : Size< i} → Stream {j} A
open Stream public

_++ˢ_ : ∀ {i A} → List A → Stream {i} A → Stream {i} A
[]        ++ˢ s = s
(a ∷ as)  ++ˢ s = a ∷ˢ (as ++ˢ s)

This fails, maybe unjustified, at

i : Size, s : Stream {i} A
  ⊢
    a ∷ˢ (λ {j : Size< i} → as ++ˢ s)

Fixed by defining the constructor by copattern matching:

record Stream {i : Size} (A : Set) : Set where
  coinductive
  field
    head  : A
    tail  : ∀ {j : Size< i} → Stream {j} A
open Stream public

_∷ˢ_ : ∀ {i A} → A → Stream {i} A → Stream {↑ i} A
head  (a ∷ˢ as) = a
tail  (a ∷ˢ as) = as

_++ˢ_ : ∀ {i A} → List A → Stream {i} A → Stream {i} A
[]        ++ˢ s = s
(a ∷ as)  ++ˢ s = a ∷ˢ (as ++ˢ s)

The ugly:

fix : ∀ {C : Size → Set}
   → (∀ i → (∀ (j : Size< i) → C j) → C i)
   → ∀ i → C i
fix t i = t i λ (j : Size< i) → fix t j

For i=0, there is no such j at runtime, leading to looping behavior.

Interaction

Issue #635 has been fixed. Case splitting does not spit out implicit record patterns any more.

  record Cont : Set₁ where
    constructor _◃_
    field
      Sh  : Set
      Pos : Sh → Set

  open Cont

  data W (C : Cont) : Set where
    sup : (s : Sh C) (k : Pos C s → W C) → W C

  bogus : {C : Cont} → W C → Set
  bogus w = {!w!}

Case splitting on w yielded, since the fix of Issue #473,

  bogus {Sh ◃ Pos} (sup s k) = ?

Now it gives, as expected,

  bogus (sup s k) = ?

Performance

As one result of the 21st Agda Implementor's Meeting (AIM XXI), serialization of the standard library is 50% faster (time reduced by a third), without using additional disk space for the interface files.

Bug fixes

Issues fixed (see bug tracker):

#1546 (copattern matching and with-clauses)

#1560 (positivity checker inefficiency)

#1584 (let pattern with trailing implicit)

2.4.2.4.md 7.6 KB História Raw