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
Table of contents
- Introduction
- What can be declared as irrelevant?
- Examples
- What can be done to irrelevant things
- What can't be done to irrelevant things
- Raw release notes
- References
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:
- Arguments of (both dependent and non-dependent) functions
- Record fields
- Postulates
- 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:
- 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