Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
The "Computational Component" section of the Type Theory - Wikipedia (as well as a few papers about cubical type theory and 2d type theory) talk about canonicity property.
There are potentially multiple ways of presenting canonicity (and I think complications depending on the theory). However, I think the simplest way to think about it is from the perspective of a programmer wanting to use the type theory to compute something. For instance, we might want to compute some natural number satisfying some specification we've come up with. So we define:
data ℕ : Type where
zero : ℕ
suc : ℕ → ℕ
These constructors we've used have meaning to us, and we want the answer to be written in terms of them. So, for instance, suc (suc (suc zero))) is a valid, meaningful result of our computation.
Canonicity says essentially that every closed computation of type ℕ we write is able to be reduced to such a meaningful numeral. Or, if we don't want to talk about 'reduction', it is "convertable" or "judgmentally equal" to such a numeral, or similar. But of course, if we're programmers, we probably want that convertability to eventually turn into reduction for at least some stuff.
The reason homotopy type theory (at least, at the time of the book) does not have this property is that there was no known computational behavior for univalence; it was just added to the theory as an 'axiom,' and you could then use it in ways where computations would just get stuck. So, in that situation, you can sometimes write closed terms of type ℕ that might look like
J (...) (ua ...) ...
But do not compute further than that, because J has no way of reducing when applied to ua .... So you can write terms that don't give you a meaningful answer.
A simpler example is, I think, also mentioned in that article. You can add some variety of excluded middle to have a 'classical' type theory. To do this, we can add an axiom like:
exm A : A + ¬ A
that says that every type either has a value or is empty. However, unless your types are quite simple, it is impossible to accurately decide such a thing, so this axiom will not be able to compute to either inl x or inr y, and case analysis on it will just get stuck.
This may not be a problem if you are just using type theory in a way analogous to formal logic. You can add axioms that get stuck, and add more axioms about the things that get stuck to prove specific things you desire, but those will also get stuck. For instance perhaps we could add:
uaId : ua id ≡ refl
uaAp : subst (λ A → A) (ua f) x ≡ f x
And so on. These will allow us to manually prove certain reduction rules, so that we can manually prove that some expression we've written is (according to our axioms) the same as some concrete number. However, for someone who desires to treat type theory more like executable mathematics that will automatically compute answers, canonicity is an important property.
A + ¬ A does not compute to either inl x or inr y? 2) What does it mean to add further axioms and get stuck?
$\endgroup$
P(n) = the Turing machine represented by n halts. Then if we use em we can get ∀ n → P(n) + ¬ P(n). Read classically this is a statement that every machine halts or doesn't, but to have computational content (in the usual sense) we must be able to decide whether each machine halts or doesn't, and that is a problem.
$\endgroup$