Why does it matter if canonicity holds for irrelevant types?

Question

Suppose you were to add a non-constructive axiom which only applies to irrelevant types, such as the irrelevance axiom. To my understanding canonicity and strong normalization are defining features of constructivity. However:

• irrelevant types don't compute by definition, so I don't think it would affect the computational properties of the type theory if the axiom doesn't compute; and
• if my understanding of conservativity is correct, then it shouldn't matter that it's non-conservative because it's definitionally proof-irrelevant.

I would expect the axiom to still break canonicity, but only for irrelevant types. Why does it matter if canonicity holds for irrelevant types? Are there any other desirable properties that it would break?

Answer 1

I will focus here on a universe of definitionally irrelevant types; let's call it SProp. In short, we can postulate any consistent SProp axiom, without breaking any constructive metatheoretic property. Formally, SProp terms are propositionally truncated, which means that no model can distinguish terms of the same SProp type. We could say that SProp terms trivially enjoy canonicity. For example, any (open) proof of t = t : SProp is definitionally equal to refl. But actually we don't really care if there is a "canonical" proof like refl, because all proofs are equal, so if any one of them is "canonical", then they all are.

Compare e.g. the treatment of negative types in canonicity proofs. We don't have to prove anything about terms of negative types; we already know that any $t : \top$ is $\mathsf{tt}$, any $t : \Pi\,A\,B$ is a $\lambda$, and any $t : \Sigma\,A\,B$ is a pairing.

Of course, if we postulate an inconsistent axiom in SProp, that breaks computational properties, since we can eliminate from $\bot$ to proof-relevant types, and define loops and closed non-canonical relevant values.

The SProp variant of the irrelevance axiom is also computationally adequate, since it's just an axiom in SProp:

data Squash (A : Set) : Prop where 
  squash : A -> Squash A

irrelevance : (A : Set) -> Squash (Squash A -> A)

This formulation seems to be equivalent to an SProp-indexed axiom of choice:

Irrelevance = {A : Set} → Squash (Squash A → A)
PropChoice  = {A : Prop}{B : Set} → (A → Squash B) → Squash (A → B)

to : Irrelevance → PropChoice
to irr {A} {B} f with irr {B}
... | squash g = squash λ a → g (f a)

from : PropChoice → Irrelevance
from pch {A} = pch λ sqa → sqa

In observational type theories, the ability to postulate SProp axioms without breaking canonicity becomes a bit more interesting, since in that setting we can eliminate from SProp propositional equality to any type.

Answer 2

Consider the following type theory:

\begin{gather} \frac{ }{\vdash G \; \mathsf{type}} \qquad \frac{ }{\vdash \Lambda \; \mathsf{type}} \\[2ex] \frac{\vdash g : G \qquad \vdash e_1 : \Lambda \qquad \vdash e_2 : \Lambda}{\vdash e_1 \, e_2 : \Lambda} \\[2ex] \frac{\vdash g : G \qquad x : \Lambda \vdash e : \Lambda}{\vdash \lambda x \,.\, e : \Lambda} \\[2ex] \frac{\vdash g : G \qquad x : \Lambda \vdash e'_1 : \Lambda \qquad \vdash e_2 : \Lambda}{\vdash (\lambda x \,.\, e'_1) \, e_2 \equiv e'_1[e_2/x] : \Lambda} \end{gather}

It is the untyped $\lambda$-calculus with a proof-irrelevant “guard” type $G$: in order to form any terms of type $\Lambda$ or to apply the $\beta$-rule, we must first exhibit a proof-irrelevant term of type $G$.

The theory has a model in which both $G$ and $\Lambda$ are interpreted as the empty set. Therefore, there are no closed terms of any type (the only types are $G$ and $\Lambda$ – we did not assume any extra structure). It is vacuously the case that every closed term is normalizing for any notion of normalization.

Observe also that in the non-empty context $z : G$ the untyped $\lambda$-calculus springs to life because $z$ can be used to justify the construction of terms and applications of the $\beta$-rule. Hence, as soon as we add a (proof-irrelevant!) constant

$$\frac{ }{\vdash g : G}$$

all hell breaks loose in the empty context (of course the untyped $\lambda$-calculus is not normalizing).

You may think the example a silly one, and I concur. However, it demonstrates a point well: the addition of a proof-irrelevant constant may change the behavior of proof-relevant closed terms.

If we wish to avoid the above travesty, we need to find a meta-theoretic property of type theories which prevents it. I would be quite impressed to see a reasonably general and non-artificial property that accomplishes the task.

It is interesting to ask whether we could modify the above example so that $G$ becomes proof-relevant. I think so, like this:

\begin{gather} \frac{ }{\vdash G \; \mathsf{type}} \qquad \frac{ }{\vdash \Lambda \; \mathsf{type}} \\[2ex] \frac{\vdash g : G \qquad \vdash e_1 : \Lambda \qquad \vdash e_2 : \Lambda}{\vdash \mathsf{app}(g, e_1, e_2) : \Lambda} \\[2ex] \frac{\vdash g : G \qquad x : \Lambda \vdash e : \Lambda}{\vdash \lambda(g, x \,.\, e) : \Lambda} \\[2ex] \frac{\vdash g_1 : G \qquad \vdash g_2 : G \qquad x : \Lambda \vdash e'_1 : \Lambda \qquad \vdash e_2 : \Lambda}{\vdash \mathsf{app}(g_1, \lambda(g_2, x \,.\, e'_1)) \, e_2 \equiv e'_1[e_2/x] : \Lambda} \end{gather}

Answer 3

One answer is that (judgmental) proof irrelevance does not correspond to computational irrelevance. Proof irrelevance means that every proof is equal in some sense. But that doesn't mean the values can't be interesting.

For instance, in something like a setoid or realizability interpretation, values of propositions like $∃n:ℕ. ...$ actually have natural numbers witnessing them; potentially multiple natural numbers. Even in such a case, the proofs are considered equal by fiat. They don't need to be represented uniquely, the system just needs to ensure that equal results are produced from any input proposition. In particular this means that implication of propositions can be witnessed by any appropriate function (i.e. not necessarily constant), since the results will also all be considered equal.

This matters if you want to extract the computational content from the propositions at a level below the surface language. You can do the calculations underlying the proofs and get some kind of actual result. The result you get will depend on the details of the proof, but you might not care so long as you get a result. An example would be Andrej Bauer's and Paul Taylor's work on computing with Dedekind reals, where the proofs involved let you calculate rational approximations. You can't do this if you add an axiom that you don't know how to calculate with.

---

However, the above is actually unrelated to your example, because Agda's irrelevant arguments are about computational irrelevance and erasure. The idea there is that we intend to actually strip the annotated things out of the program. That can be related to the above, because stripping all the information out of a proof is a way to make it irrelevant in the above sense, but in general you can have either without the other, I believe.

Even computational irrelevance is subtle, though, because in type theories it matters when you plan to erase things. There are at least two stages of evaluation in dependent type theories. One is type checking, and the other is running the 'program' you have specified. The big difference is that the former operates on open terms with variables, while the latter generally happens on something corresponding to closed terms.

So, one issue is that things that are computationally irrelevant during closed term evaluation are not irrelevant during open term evaluation. The obvious traditional example is types. It's desirable to not be calculating the type of everything during program execution, but types matter while you're checking them. And there are many other examples of things that are computationally irrelevant during closed term evaluation, but might cause problems if they're erased during open term evaluation.

The justification behind irrelevant projections is also that there is only one 'stage' of irrelevance; once you've shifted to the erased part, all irrelevant things become relevant, and there are no further phase distinctions. But one might want to have multiple stages of computational (ir)relevance that don't collapse. That could make it matter whether you add other non-computational axioms as well.

In the Agda case, I'm not sure it really runs much deeper than the feature being a frequent source of bugs, though.