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.

  • Would you please explain exactly what this property is and what does it mean in type theory?
  • Why and how is it lost in the Homotopy Type Theory with the univalent axiom?


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.

  • 1
    $\begingroup$ Thanks Dan. Your description was clear. But would you please elaborate further about following two parts: 1) Why 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$
    – al pal
    Aug 22 '19 at 4:25
  • $\begingroup$ I added some explanation. Does that help? $\endgroup$
    – Dan Doel
    Aug 22 '19 at 12:43
  • $\begingroup$ Thanks, and when you say "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.", is it because in general one can not find a value nor prove that there is no value constructively, for every type? $\endgroup$
    – al pal
    Aug 22 '19 at 15:52
  • 2
    $\begingroup$ If your type theory is capable of serving as a sort of mathematical logic, then you'll probably be able to construct predicates like 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$
    – Dan Doel
    Aug 22 '19 at 23:24
  • 1
    $\begingroup$ There are ways of giving more computational content to classical statements like that (like, assume it doesn't halt, and if someone contradicts you go back and change your decision). However, those break other nice properties of the theory (like confluence/determinism). $\endgroup$
    – Dan Doel
    Aug 22 '19 at 23:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.