# Irrelevance

See the official user manual for the most up-to-date version of the information on this page.

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
```

## 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!
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
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'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 : ℕ → .ℕ

-- 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 (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:

• irrelevant record fields and non-dependent function arguments
• add irrelevant functions and postulates
• projections generated automatically for irrelevant fields
• dependent irrelevant function types
• adjusted module generation for records with only irrelevant fields
• dropped interal erasing of irrelevant thing