Irrelevance

Since version 2.2.8 Agda supports irrelevancy annotations. The general rule is that anything prepended by a dot (.) is marked irrelevant, which means that it will only be typechecked but never evaluated.

Note

This section is about compile-time irrelevance. See Run-time Irrelevance for the section on run-time irrelevance.

The more recent Prop serves a similar purpose and can be used to simulate irrelevance.

Motivating example

One intended use case of irrelevance is data structures with embedded proofs, like sorted lists.

data _≤_ : Nat → Nat → Set where
  zero≤   : {n : Nat} → zero ≤ n
  suc≤suc : {m n : Nat} → m ≤ n → suc m ≤ suc n
postulate
  p₁  : 0 ≤ 1
  p₂  : 0 ≤ 1
module No-Irrelevance where
  data SList (bound : Nat) : Set where
    []    : SList bound
    scons : (head : Nat)
          → (head ≤ bound)
          → (tail : SList head)
          → SList bound

Usually, when we define datatypes with embedded proofs we are forced to reason about the values of these proofs. For example, suppose we have two lists l₁ and l₂ with the same elements but different proofs:

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

It’s not so easy! Agda gives us an error:

p₁ != p₂ of type 0 ≤ 1
when checking that the expression refl has type l₁ ≡ l₂

We can’t show that l₁ ≡ l₂ by refl when p₁ and p₂ are relevant. Instead, we need to reason about proofs of 0 ≤ 1.

postulate
  proof-equality : p₁ ≡ p₂

Now we can prove l₁ ≡ l₂ by rewriting with this equality:

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

Reasoning about equality of proofs becomes annoying quickly. 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. We can use irrelevance annotations to tell Agda we don’t care about the values of the proofs:

data SList (bound : Nat) : Set where
  []    : SList bound
  scons : (head : Nat)
        → .(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

Irrelevant function types

For starters, consider irrelevant non-dependent function types:

f : .A → B

This type implies that f does not depend computationally on its argument.

What can be done to irrelevant arguments

Example 1. We can prove that two applications of an unknown irrelevant function to two different arguments are equal.

-- an unknown function that does not use its second argument
postulate
  f : {A B : Set} -> A -> .B -> A
-- the second argument is irrelevant for equality
proofIrr : {A : Set}{x y z : A} -> f x y ≡ f x z
proofIrr = refl

Example 2. We can use irrelevant arguments as arguments to other irrelevant functions.

id : {A B : Set} -> (.A -> B) -> .A -> B
id g x = g x

Example 3. We can match on an irrelevant argument of an empty type with an absurd pattern ().

data ⊥ : Set where
zero-not-one : .(0 ≡ 1) → ⊥
zero-not-one ()

What can’t be done to irrelevant arguments

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

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

Variable m is declared irrelevant, so it cannot be used here
when checking that the expression m has type Nat

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

bad : Nat → .Nat
bad n = 1

Invalid dotted expression
when checking that the expression .Nat has type Set _47

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

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

Cannot pattern match against irrelevant argument of type Nat
when checking that the pattern zero has type Nat

Example 4. We also can’t match on an irrelevant record (see Record Types).

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
irrElim : {A : Set} {B : A → Set} → .(Σ A B) → _
irrElim (a , b) = ?

Cannot pattern match against irrelevant argument of type Σ A B
when checking that the pattern a , b has type Σ A B

If this were allowed, b would have type B a but this type is not even well-formed because a is irrelevant!

Irrelevant declarations

Postulates and functions can be marked as irrelevant by prefixing the name with a dot when the name is declared. Irrelevant definitions can only be used as arguments of functions of an irrelevant function type .A → B.

Examples:

.irrFunction : Nat → Nat
irrFunction zero    = zero
irrFunction (suc n) = suc (suc (irrFunction n))
postulate
  .assume-false : (A : Set) → A

An important example is the irrelevance axiom irrAx:

postulate
  .irrAx : ∀ {ℓ} {A : Set ℓ} -> .A -> A

This axiom is not provable inside Agda, but it is often very useful when working with irrelevance. The irrelevance axiom is a form of non-constructive choice.

Irrelevant record fields

Record fields (see Record Types) can be marked as irrelevant by prefixing their name with a dot in the definition of the record type. Projections for irrelevant fields are only created if option --irrelevant-projections is supplied (since Agda > 2.5.4).

Example 1. A record type containing pairs of numbers satisfying certain properties.

record InterestingNumbers : Set where
  field
    n      : Nat
    m      : Nat
    .prop1 : n + m ≡ n * m + 2
    .prop2 : suc m ≤ n

Example 2. For any type A, we can define a ‘squashed’ version Squash A where all elements are equal.

record Squash (A : Set) : Set where
  constructor squash
  field
    .unsquash : A
open Squash
.example : ∀ {A} → Squash A → A
example x = unsquash x

Example 3. We can define the subset of x : A satisfying P x with irrelevant membership certificates.

record Subset (A : Set) (P : A -> Set) : Set where
  constructor _#_
  field
    elem         : A
    .certificate : P elem
.certificate : {A : Set}{P : A -> Set} -> (x : Subset A P) -> P (Subset.elem x)
certificate (a # p) = irrAx p

Example 4. Irrelevant projections are justified by the irrelevance axiom.

.unsquash' : ∀ {A} → Squash A → A
unsquash' (squash x) = irrAx x
.irrAx' : ∀ {A} → .A → A
irrAx' x = unsquash (squash x)

Like the irrelevance axiom, irrelevant projections cannot be reduced.

Dependent irrelevant function types

Just like non-dependent functions, we can also make dependent functions irrelevant. The basic syntax is as in the following examples:

f : .(x y : A) → B
f : .{x y z : A} → B
f : .(xs {ys zs} : A) → B
f : ∀ x .y → B
f : ∀ x .{y} {z} .v → B
f : .{{x : A}} → 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] = C x, with C : .A → Set.

Dependent irrelevance allows us to define the eliminator for the Squash type:

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)).

Irrelevant instance arguments

Contrary to normal instance arguments, irrelevant instance arguments (see Instance Arguments) are not required to have a unique solution.

record ⊤ : Set where
  instance constructor tt
NonZero : Nat → Set
NonZero zero    = ⊥
NonZero (suc _) = ⊤
pred′ : (n : Nat) .{{_ : NonZero n}} → Nat
pred′ zero {{}}
pred′ (suc n) = n
find-nonzero : (n : Nat) {{x y : NonZero n}} → Nat
find-nonzero n = pred′ n