Irrelevance

TOC

This document has been extracted from a literate Agda file, which was tested with Agda 2.3.0. It uses the standard library, the following imports should be used to check this file:

  open import Data.Nat
  open import Data.Product
  open import Relation.Binary.PropositionalEquality

Table of contents

  1. Introduction
    1. Motivating example
  2. What can be declared as irrelevant?
  3. Examples
    1. Function arguments
    2. Record fields
    3. Postulates
    4. Functions
  4. What can be done to irrelevant things
  5. What can't be done to irrelevant things
  6. Raw release notes
    1. Agda 2.2.8 release notes
      1. Irrelevant contexts
      2. Irrelevant record fields
      3. Final warning
    2. Agda 2.2.10 release notes
      1. Irrelevant postulates and functions
      2. Projections from irrelevant record fields
    3. Agda 2.3.0 release notes
      1. Dependent irrelevant function types.
      2. Records with only irrelevant fields
      3. No more erasing
      4. experimental-irrelevance flag
  7. References
    1. History of changes of the support for irrelevance in Agda:

Introduction

Proof irrelevant function types.

Motivating example

Since version 2.2.8 Agda supports irrelevancy annotations.

For starters, consider irrelevant non-dependent function types:

 f : .A → B

This type implies that f does not depend computationally on its argument. One intended use case is data structures with embedded proofs, like sorted lists:

  postulate
    p₁  : 0 ≤ 1
    p₂  : 0 ≤ 1

  data SList (bound : ℕ) : Set where
    []    : SList bound
    scons : (head : ℕ) →
          .(head ≤ bound) →        -- note the dot!
          (tail : SList head) →
          SList bound

The effect of the irrelevant type in the signature of scons is that scons’s second argument is never inspected after Agda has ensured that it has the right type. The type-checker ignores irrelevant arguments when checking equality, so two lists can be equal even if they contain different proofs:

  l₁ : SList 1
  l₁ = scons 0 p₁ []

  l₂ : SList 1
  l₂ = scons 0 p₂ []

  l₁≡l₂ : l₁ ≡ l₂
  l₁≡l₂ = refl

Note that if we haven't marked the second argument as irrelevant, we would have to provide a proof of p₁ ≡ p₂ (see example below). We would like to avoid this kind of reasoning about proofs here - in this case we only care that a proof of head ≤ bound exists, i.e. any proof suffices.

Example. This is what we would have to do if we haven't taken advantage of irrelevancy:

  postulate
    p₁  : 0 ≤ 1
    p₂  : 0 ≤ 1

  data SList (bound : ℕ) : Set where
    []    : SList bound
    scons : (head : ℕ) →
          (head ≤ bound) →        -- no dot
          (tail : SList head) →
          SList bound

  l₁ : SList 1
  l₁ = scons 0 p₁ []

  l₂ : SList 1
  l₂ = scons 0 p₂ []

Now suppose we want to prove that l₁ and l₂ are equal:

  l₁≡l₂ : l₁ ≡ l₂
  l₁≡l₂ = refl

Not so easy!

The goal is scons 0 p₁ [] ≡ scons 0 p₂ [].
We can't show that just by refl when p₁ and p₂ are relevant!

We need to reason about proofs of 0 ≤ 1.

  postulate
    proof-equality : p₁ ≡ p₂

Now we'll be good.

  l₁≡l₂ : l₁ ≡ l₂
  l₁≡l₂ rewrite proof-equality = refl

What can be declared as irrelevant?

The following things can be declared irrelevant:

  1. Arguments of (both dependent and non-dependent) functions
  2. Record fields
  3. Postulates
  4. Functions

Syntax for these is shown in examples below.

Examples

The general rule is that anything prepended by a dot (.) is marked irrelevant.

Function arguments

The basic syntax:

 -- non-dependent case
 f : .A → B

 -- dependent case
 .(x y : A) → B    
 .{x y z : A} → B
 ∀ x .y → B        
 ∀ x .{y} {z} .v → B

Record fields

  record InterestingNumbers : Set where
    field
      n      : ℕ
      m      : ℕ
      .prop1 : n + m ≡ n * m + 2
      .prop2 : n > m

Postulates

  postulate
    .assume-false : (A : Set) → A

Functions

We marked function arguments as irrelevant above, here we show how to declare the function itself as irrelevant.

  .irrFunction : ℕ → ℕ
  irrFunction zero    = zero
  irrFunction (suc n) = suc (suc (irrFunction n))

What can be done to irrelevant things

What can't be done to irrelevant things

None of the example in this section works.

Example 1. You can't use an irrelevant value in a non-irrelevant context

 bad-plus : ℕ → .ℕ → ℕ
 bad-plus n m = m + n

 -- Agda's error message:
 Variable m is declared irrelevant, so it cannot be used here
 when checking that the expression m has type ℕ

Example 2. You can't declare the function's return type as irrelevant:

  bad : ℕ → .ℕ
  bad n = 1

  -- Agda's error message:
  .ℕ is not a valid expression.
  when scope checking .ℕ

Example 3. You can't pattern match on an irrelevant value:

  badMatching : ℕ → .ℕ → ℕ
  badMatching n zero    = n
  badMatching n (suc m) = n

  -- Agda's error message:
  Cannot pattern match zero against irrelevant type ℕ
  when checking that the clause badMatching n zero = n has type
  ℕ → .ℕ → ℕ

Raw release notes

Agda 2.2.8 release notes

Irrelevant contexts

TODO: Can we define/characterise irrelevant contexts?

Irrelevant arguments can only be used in irrelevant contexts. Consider the following subset type:

  data Subset (A : Set) (P : A → Set) : Set where
    _#_ : (elem : A) → .(P elem) → Subset A P

The following two uses are fine:

  elimSubset : ∀ {A C : Set} {P} →
               Subset A P → ((a : A) → .(P a) → C) → C
  elimSubset (a # p) k = k a p

  elem : {A : Set} {P : A → Set} → Subset A P → A
  elem (x # p) = x

However, if we try to project out the proof component, then Agda complains that “variable p is declared irrelevant, so it cannot be used here”:

  prjProof : ∀ {A P} (x : Subset A P) → P (elem x)
  prjProof (a # p) = p

Matching against irrelevant arguments is also forbidden, except in the case of irrefutable matches (record constructor patterns which have been translated away). For instance, the match against the pattern (p , q) here is accepted:

  elim₂ : ∀ {A C : Set} {P Q : A → Set} →
          Subset A (λ x → Σ (P x) (λ _ → Q x)) →
          ((a : A) → .(P a) → .(Q a) → C) → C
  elim₂ (a # (p , q)) k = k a p q

Absurd matches () are also allowed.

Irrelevant record fields

Note that record fields can also be irrelevant. Example:

  record SubsetRecord (A : Set) (P : A → Set) : Set where
    constructor _#_
    field
      elemRec : A
      .proof  : P elemRec

Irrelevant fields are never in scope, neither inside nor outside the record. This means that no record field can depend on an irrelevant field, and furthermore projections are not defined for such fields. Irrelevant fields can only be accessed using pattern matching, as in elimSubset above.

Final warning

Irrelevant function types were added very recently, and have not been subjected to much experimentation yet, so do not be surprised if something is changed before the next release. For instance, dependent irrelevant function spaces (.(x : A) → B) might be added in the future.

Agda 2.2.10 release notes

Irrelevant postulates and functions

Postulates and functions can be marked as irrelevant by prefixing the name with a dot when the name is declared. Example:

  postulate
    .irrelevant : {A : Set} → .A → A

Irrelevant names may only be used in irrelevant positions or in definitions of things which have been declared irrelevant.

Projections from irrelevant record fields

The axiom irrelevant above can be used to define a projection from an irrelevant record field:

  data Subset (A : Set) (P : A → Set) : Set where
    _#_ : (a : A) → .(P a) → Subset A P


  elem' : ∀ {A P} → Subset A P → A
  elem' (a # p) = a

  .certificate : ∀ {A P} (x : Subset A P) → P (elem x)
  certificate (a # p) = irrelevant p

The right-hand side of certificate is relevant, so we cannot define

  certificate (a # p) = p

(because p is irrelevant). However, certificate is declared to be irrelevant, so it can use the axiom irrelevant. Furthermore the first argument of the axiom is irrelevant, which means that irrelevant p is well-formed.

As shown above the axiom irrelevant justifies irrelevant projections. Previously no projections were generated for irrelevant record fields, such as the field certificate in the following record type:

  record Subset (A : Set) (P : A → Set) : Set where
    constructor _#_
    field
      elem         : A
      .certificate : P elem

Now projections are generated automatically for irrelevant fields (unless the flag --no-irrelevant-projections is used). Note that irrelevant projections are highly experimental.

Agda 2.3.0 release notes

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:

  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

  (ih : (a : A) → P (squash a)).

Records with only irrelevant fields

The following now works:

  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:

  module IsEquivalence {A : Set} {_≈_ : A → A → Set}
    .(r : IsEquivalence {A = A} _≈_) where
    …

No more erasing

Irrelevant things are no longer erased internally. This means that they are printed as ordinary terms, not as “_” as before.

experimental-irrelevance flag

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.

References

History of changes of the support for irrelevance in Agda:

Version-2-2-8:

  • irrelevant record fields and non-dependent function arguments

Version-2-2-10:

  • add irrelevant functions and postulates
  • projections generated automatically for irrelevant fields

Version-2-3-0:

  • dependent irrelevant function types
  • adjusted module generation for records with only irrelevant fields
  • dropped interal erasing of irrelevant thing