Canonicity

Idea

Canonicity is a property of a type theory equipped with a notion of computation. It states that every closed term of a designated observable type reduces, or is judgmentally equal, to a canonical form of that type.

Canonical forms are specified by the underlying type theory. They are usually introduction-headed normal form whose components are themselves canonical where appropriate.

Canonicity is weaker than normalization.

• Normalization says that every term reduces to a normal form.
• Canonicity says that closed normal terms of certain types have the expected canonical shape.

A normal form may instead be neutral, meaning that its computation is blocked by a variable or opaque constant. Strong canonicity says that this cannot happen for closed terms of observable data types.

Examples

• For natural numbers, the canonical forms are $0$, $\mathrm{suc}(0)$, $\mathrm{suc}(\mathrm{suc}(0))$, and so on.
• For ordinary first-order inductive types, canonical forms are constructor-headed terms whose arguments are canonical.
• For dependent function types, canonical forms are lambda abstractions $\lambda x.t$.
• For dependent sum types, canonical forms are pairs $(a,b)$.
• For ordinary intensional identity types, the only introduction form is $\mathrm{refl}$. This must be modified in theories with primitive paths, higher inductive types, or additional equality axioms.
• For universes, canonical forms are codes or type-forming expressions such as dependent products, dependent sums, and inductive type codes, depending on the presentation of the universe.

Strengths

Several versions of canonicity should be distinguished.

Judgmental Canonicity

Every closed term is judgmentally equal to a canonical form. For example,

$$⊢n:\mathbb{N}⟹n\equiv {\mathrm{suc}}^k(0)$$

for some $k$.

Propositional Canonicity

Every closed term is propositionally equal to a canonical form:

$$⊢n:\mathbb{N}⟹{\Sigma }_{k:\mathbb{N}}n={\mathrm{suc}}^k(0).$$

Homotopy Canonicity

In a higher type theory, every closed term is connected to a canonical form by a path. This may hold even when the term does not judgmentally compute to that form.

Transports

Canonical does not simply mean that a term contains no transports.

In an open context, a transport along a variable path may be a neutral normal form:

$$p:x{=}_{A}y⊢{\mathrm{transport}}_B(p,u):B(y).$$

Such a term may therefore occur inside an open normal form. Strong canonicity for closed data requires that closed transports compute sufficiently far that they cannot leave a closed natural number or Booleans stuck.

Quotients And Higher Inductive Types

For quotient or higher inductive types, canonical forms are constructor forms modulo the specified path constructors. There may be no preferred representative of a quotient class.

An axiomatic presentation may provide only propositional or homotopy canonicity. A computational or cubical presentation can sometimes provide judgmental canonicity by giving paths, coercions, and higher constructors operational behavior.

Coinductive Types

A coinductive object need not reduce to a finite complete canonical form. The corresponding property is usually called productivity: every finite observation of a closed coinductive object computes in finite time.

Thus, for a stream $s$, its head and every finite prefix should be computable, even though the entire stream is infinite.

Related Concepts

Closed Term
Dependent Product
Dependent Sum
Identity Type
Inductive Type
Natural Number
Type Theory

References

https://www.cse.chalmers.se/~coquand/canorm1.pdf