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

## 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
→ 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
→ .(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
```

## 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
```
```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 (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.

## 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
.proof : A

open Squash

.unsquash : ∀ {A} → Squash A → A
unsquash x = proof 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
```

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