# What is a non-canonical term?

I've heard the phrase used in relation to comparing proof assistants, but I don't understand what it means.

For example, for introducing an instance of coinductive types, Agda uses destructors and Idris uses constructors...and having used Idris I was thinking that Agda's approach was non-canonical in that the terms can't be broken down into constructors nor do they always progress to whnf. But I have been told this is not correct. So what is a non-canonical term?

To give an example (following ice1000's post):

Yes (to ice1000), this is the question. And here's an example in Idris:

data CoNat: Type where
Zero : CoNat
Succ : Inf CoNat -> CoNat


With corresponding code in Agda:

record ℕ∞ : Set where
coinductive
field
prd∞ : Maybe ℕ∞


But Agda has elements that don't appear in the Idris version

record ℕ∞ : Set where
coinductive
field
prd∞ : Maybe ℕ∞

+∞ : ℕ∞ → ℕ∞ → ℕ∞
prd∞ (m +∞ n) with prd∞ m
... | nothing = prd∞ n
... | just m' = just (m' +∞ n)

∞ : ℕ∞
prd∞ ∞ = just ∞

noncanonical? : ℕ∞
noncanonical? = ∞ +∞ ∞


So I was thinking that such elements must be non-canonical as they are not present in the Idris version!! If they are not non-canonical because they are defined in terms of the 'destructors' then what would be an example of a non-canonical instance???

• I think it would be better to ask what is a canonical term, and maybe ncatlab.org/nlab/show/canonical+form is helpful. May 30 at 23:24
• What do you mean by "they are not present in the Idris version"? You can definitely define infinity = Succ infinity and then infinity2 = infinity + infinity. May 31 at 9:35
• But in Idris it makes no (less?) difference in that infinity + infinity will always spit out succ (infinity)+ when asked for the next constructor. So it acts the same as infinity anyway, which spits out succ(infinity). Whereas in Agda they act very differently, you end up with two different things in your hands, an infinity and an infinity + infinity, and it's hard to get them to act the same. May 31 at 14:13
• Aside : they are cubically path equivalent in Agda... +inf : (n : ℕ∞) -> n +∞ ∞ ≡ ∞ prd∞ (+inf n i) with prd∞ n ... | just x = just (+inf x i) ... | nothing = just ∞ May 31 at 14:49
• @RobertWatson infinity+infinity and infinity are also bisimilar (the intended propositional equality for coinductive types), IMO May 31 at 18:26

Your claim that Agda has element which Idris doesn't have is not true. Here's an Idris-equivalent I came up with:

add : Inf CoNat -> Inf CoNat -> Inf CoNat
add (Delay Zero) b = b
add (Delay (Succ a)) b = Succ (add a b)

inf : CoNat
inf = Succ inf

infinf : CoNat
infinf = add inf inf


I think your question is about canonical forms of coinductive types. In Agda's coinduction, the introduction form of a codata is a "(co) pattern matching on how you destruct it", not constructing something. So, the fields are kind of like "under a binder", thus not evaluating them is fine.

Also note that coinductive types have no $$\eta$$ laws, i.e. it does not hold definitionally that $$a \equiv \text{record}\{p=a.p\}$$. This means you have no way to evaluate the fields except projecting them out. I think this idea replaces Idris' way (and also Agda's old way) of "later modality"-sque approach, which uses a "guard" instead of a closure.

By the way, I have the impression that the Idris approach has some limitations. Long time ago Agda uses the same idea (with explicit musical notations), but Andras Abel invented copatterns and guardedness (also sized-types) and I think everyone's using it now as G. Allais said in the comments, people tend to use copatterns nowadays because they are more beautiful.

• I think we're using copatterns because they more satisfyingly show the duality between inductive/coinductive types but I don't believe guardedness is any more powerful using copatterns than musical notations. Sized types are fantastic in that they provide a more compositional notion of guarded calls but their implementation is unfortunately currently unsound. May 31 at 9:28
• I think it may be a bit much to say that sized types are fantastic except for their implementation --- I don't think there is any known theory of sized types that does the things that people need them to do. There's a reason the unsound implementation has been hard to fix --- I think it's quite unclear what to replace it with. Jun 6 at 9:01

The notion of a canonical term is an additional structure on type theory which must be specified. Informally speaking, it means something like "special nice form that we like very much". Quite often canonical terms are "computed all the way", i.e., we cannot reduce them further.

In almost all cases it is super-easy to provide non-canonical terms, for instance, given any type A and any term a : A, the term (λ x → x) a is non-canonical (because we can make one step of computation to obtain a – which may or may not be canonical, depending on a).

• If 'computed all the way' is canonical form, then how would you define normal forms? Jun 2 at 3:14
• I think there are two ways to define normal forms: as stuck terms (things that do not compute further) and as values (usually, values are either canonical forms with recursively normal subterms, or neutral forms, eg an elimination context blocked by a variable with recursively normal components). Then the progress theorem of programming language theory tells you that on well-typed terms, both notions correspond: a term is either a value or evaluates further. Jun 2 at 13:19
• If I remember my symbolic computation classes well enough, canonical forms are representative of equivalence classes with respect to the equivalence relation generated by rewriting rules, while normal forms have no further rewriting steps. Jun 3 at 17:28