Agda.TypeChecking.Irrelevance

Compile-time irrelevance.

In type theory with compile-time irrelevance à la Pfenning (LiCS 2001), variables in the context are annotated with relevance attributes. @ Γ = r₁x₁:A₁, ..., rⱼxⱼ:Aⱼ To handle irrelevant projections, we also record the current relevance attribute in the judgement. For instance, this attribute is equal to to Irrelevant if we are in an irrelevant position, like an irrelevant argument. Γ ⊢r t : A Only relevant variables can be used: @

(Relevant x : A) ∈ Γ -------------------- Γ ⊢r x : A @ Irrelevant global declarations can only be used if r = Irrelevant@.

When we enter a r'-relevant function argument, we compose the r with r' and (left-)divide the attributes in the context by r'. @ Γ ⊢r t : (r' x : A) → B r' Γ ⊢(r'·r) u : A --------------------------------------------------------- Γ ⊢r t u : B[u/x] No surprises for abstraction: @

Γ, (r' x : A) ⊢r : B ----------------------------- Γ ⊢r λxt : (r' x : A) → B @@

This is different for runtime irrelevance (erasure) which is `flat', meaning that once one is in an irrelevant context, all new assumptions will be usable, since they are turned relevant once entering the context. See Conor McBride (WadlerFest 2016), for a type system in this spirit:

We use such a rule for runtime-irrelevance: @ Γ, (q q') x : A ⊢q t : B ------------------------------ Γ ⊢q λxt : (q' x : A) → B @

Conor's system is however set up differently, with a very different variable rule:

@@

(q x : A) ∈ Γ -------------- Γ ⊢q x : A

Γ, (q·p) x : A ⊢q t : B ----------------------------- Γ ⊢q λxt : (p x : A) → B

Γ ⊢q t : (p x : A) → B Γ' ⊢qp u : A ------------------------------------------------- Γ + Γ' ⊢q t u : B[u/x] @@