What are the complex induction patterns supported by Agda?

Question

A question was recently asked on the Coq-club mailing list on Coq rejecting a nastily nested inductive type. We encountered a similar difficulty while trying to port code from Agda to Coq: Agda accepts the following

record Foo (x : Set -> Set) :  Set where

data Bar : Set -> Set where
  bar : Bar (Foo Bar)

while Coq rejects

Record Foo (x : Type -> Type) : Type := {}.

Fail Inductive Bar : Type -> Type :=
    | bar : Bar (Foo Bar).
(*Non strictly positive occurrence of "Bar" in "Bar (Foo Bar)".*)

It seems like Coq does not accept nested inductive types in indices, while Agda does.

So I tried to look up what kind of complex induction pattern (induction-induction, induction-recursion, nestedness…) Agda exactly allows. I found the manual page on mutual recursion, which gives some examples, but is rather vague… Is there any more precise reference on what Agda allows and forbids? And, ideally, some hint as to why the allowed things are ok/have a semantic?

Answer 1

I try to write about what's supported in Agda and the semantics that we have (or don't have) for it. Disclaimers:

• I'm not an expert on the relevant parts of the Agda source code, I mostly write here as an Agda user, so I might make mistakes. Corrections are welcome.
• I don't write about coinduction. It adds many new weird and interesting feature interactions, but I'm not as nearly as experienced with coinduction as with induction in Agda.
• I don't write about erasure, irrelevance or the flat modality. I've never used these.
• I don't write much about cubical features. They don't yet work well together with many inductive features, e.g. indexed inductive types break canonicity in the 2.6.3 version of cubical Agda. The most general rigorous specification of cubical (higher) inductive types so far is in Evan Cavallo's thesis, and that only covers plain indexed HITs (no IR, no induction-induction, no nesting).

I also don't write much about dependent pattern matching. It is a powerful and complicated feature, but, perhaps surprisingly, I do not think that it's a source of weirdness and exotic features. The --without-K option precisely captures the UIP and non-UIP behaviors, and everything works generally as expected.

1. What's in Agda

---

It's a fun exercise to try to summarize this in one phrase. I'd say that Agda supports

Set/Prop-sorted non-interleaved structural inductive-inductive-recursive types, nested with simple first-order polarities

(Disregarding the cubical mode).

I'll expand on what the above means, but first let's do an overview of inductive signatures. In a nutshell, an Agda inductive signature is a list where each entry is one of four possible things:

1. A declaration of a type constructor (sort). Each declaration has a telescope of parameters, a telescope of indices and a return sort which is either Set i or Prop i. In --without-K mode, the return universe size must be large enough to accommodate the index telescope.
2. A declaration of a definition.
3. The specification of all constructors of a previously declared sort.
4. The body of a previously declared definition.

All signature entries are well-typed modulo all previously declared symbols and the definitional equalities stemming from definition bodies. Moreover, a signature is valid only if

• All inductive types are strictly positive. This depends on polarities and positivity checking.
• All definitions are total. This depends on termination checking.
• All inductive types return in a universe which is large enough to accommodate all fields of all constructors of the type.

Set/Prop-sorted

We can freely mix Set and Prop sorts, where Prop contains definitionally irrelevant types. This has not been described in any publication. I think that this is a fairly tame feature compared to some of the others, in the sense that I don't see any issue with computational adequacy (e.g. canonicity), and it shouldn't be difficult to handle in semantics.

Non-interleaved

Agda mandates that all constructors of a sort are specified together. The following can't be expressed:

A  : Set
B  : A → Set
C  : (a : A) → B a → Set
a1 : A
b  : B a1
a2 : C a1 b → A

The interleaved mutual keyword also doesn't allow this; it's merely syntactic sugar which desugars to forward-declared signatures. The problem here is that each constructor depends on the previously declared ones, so they can't be reordered. However, Szumi Xie discovered that we can convert this (and every analogous example) to a non-interleaved version by pushing all sorts inside a Tarski-style "universe":

data U  : Set
data El : U → Set

data U where
  A : U
  B : El A → U
  C : (a : El A) → El (B a) → U

data El where
  a1 : El A
  b  : El (B a1)
  a2 : El (C a1 b) → El A

I note though that while initial algebras can be derived this way, de-interleaving changes the presented theory itself (notions of algebras are different).

Also, this technique does not (fully) work with mixed Set/Prop induction, because we have to choose a single universe for El.

Structural

Agda functions are defined using structural recursion, instead of eliminators. In simple cases, the two approaches coincide, but in Agda's generality, they don't. We will see examples later.

Agda uses lexicographic recursion, which implies that multiple function arguments are considered simultaneously in termination checking. Contrast this to Coq where there's at most one structurally decreasing argument. When we specify constructors of a sort, we extend the structural ordering relation on types by positing that every constructor is larger than its fields.

(Side comment: predicativity affects structural ordering, because an impredicative function is not necessarily larger than its result values. This is relevant in Coq but not in Agda).

Inductive-inductive-recursive

Clearly, Agda includes the inductive-inductive and inductive-recursive types from the literature, but it includes more than that; see examples later.

Nested with simple first-order polarities

Agda supports nested induction. The classic example:

data Tree (A : Set) : Set where
  node : A → List (Tree A) → Tree a

Here we refer to a pre-existing List type former. But we can use any type former in scope in a nested way:

data Bush (A : Set) : Set where
  nil  : Bush A
  cons : A → Bush (Bush A) → Bush A

The most general specification of nested induction that I know about is by Johan & Polonsky. But this only covers parameterized finitary algebraic data types, a tiny subset of Agda. The positivity complications are sidestepped by only having finitary types (no function types are allowed in signatures). In ibid. the following is accepted:

data Fix f = Fix (f (Fix f))

The reason is that the type language only allows strictly positive instantiations for f. In Agda, this is not accepted. Instead there's positivity checking and a system of polarities. Like termination checking, positivity checking can look into all definitions and types in a signature.

Any function-typed symbol can have a polarity for each argument. Polarities are constant, positive, strictly positive, negative and invariant. Function arguments with arbitrary types can have polarity. Polarities are simply typed and first-order, in the sense that they are concrete and and non-dependent for each argument. For example, it is not expressible that the polarity of a parameterized type depends on parameter values. The following fails to check:

data A (b : Bool)(X : Set) : Set where
  a : if b then X else (X → X) → A b X

data B : Set where
  b : A true B → B

It works though when A is a plain definition, because while Agda only considers parameter polarities for data, it does unfold definitions:

A : Bool → Set → Set
A b X = if b then X else (X → X)

data B : Set where
  b : A true B → B

What about the strength of nested induction compared to non-nested induction? We don't know much about this in the generality of Agda, and from what I've heard, not even in the generality of Coq. We do know that nested induction allows construction of some types which are otherwise not constructible. For example, infinitary quotient inductive types are not constructible from inductive types and quotients, but if we can use nested quotients, they actually are.

2. Exotic features

---

Let's look at some notable concrete features which fall out from the Agda implementation.

Recursion-recursion

This feature has no semantics in the literature. The name "recursive-recursive" was coined by Fredrik Forsberg, as a characterization of inductive-inductive eliminators, but the weird part here is that recursion-recursion works in Agda wholly separately of induction-induction. Take this ordinary mutual inductive definition:

data Con : Set
data Ty  : Set

data Con where
  ∙ : Con
  _,_ : Con → Ty → Con

data Ty where
  Pi  : Con → Ty → Ty → Ty
  U   : Con → Ty
  El  : Con → Ty

This is intended to be "raw syntax" for some toy type theory. Now, we want to specify well-formedness for contexts and types. We want to specify that U Γ is a type in Γ, and El Γ is a type in (Γ , U). We define well-formedness predicates by recursion:

open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Unit

WfCon : Con → Set
WfTy  : ∀ Γ → WfCon Γ → Ty → Set

WfCon ∙       = ⊤
WfCon (Γ , A) = Σ (WfCon Γ) λ Γw → WfTy Γ Γw A

WfTy Γ Γw (Pi Γ' A B) = Γ ≡ Γ' × Σ (WfTy Γ Γw A) λ Aw → WfTy (Γ , A) (Γw , Aw) B
WfTy Γ Γw (U Γ')      = Γ ≡ Γ'
WfTy Γ Γw (El Γ')     = Γ ≡ (Γ' , U Γ')

Agda accepts this, but it cannot be defined directly using the elimination principle of Con and Ty! The problem is that the type of WfTy refers to WfCon, but no such dependency is possible in the eliminator. Notions of "elimination" and "structural recursion" diverge here.

Notably, much of the infamously tedious boilerplate in the initiality constructions is for recovering recursive-recursive definitions from the elimination principles of untyped syntax.

This is related to the construction of inductive-inductive types: we represent inductive-inductive types using mutually inductive "raw terms" together with well-formedness predicates. The bulk of the work is to show that recursion-recursion is derivable for the ordinary mutual inductive terms.

• We know that finitary inductive-inductive types are constructible from UIP, funext and plain induction.
• We reasonably conjecture that infinitary inductive-inductive types are constructible from UIP, funext, SProp, propext, quotients and WISC.

But we know pretty much nothing --without-K. Except, if we throw recursion-recursion in the mix, it looks like all inductive-indutive types are constructible! This is unpublished and rather fuzzy, because we don't even have a specification of recursion-recursion, but I'm fairly confident in it. I conjecture that neither recursion-recursion nor induction-induction are derivable --without-K, in the absence of some other unknown features.

Double induction-recursion

The definition of universes using induction-recursion is well-known. But what about universes of setoids, where every represented type is equipped with an equivalence relation? This is required when we want to model an observational type theory. There are several ways to do it in Agda; here's a minimal incomplete example.

open import Data.Nat
open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Data.Product

data U : Set
U~     : U → U → Set
reflU  : ∀ {A} → U~ A A
El     : U → Set
El~    : ∀ {A A'} → U~ A A' → El A → El A' → Set

resp~ : ∀ {A} → (El A → U) → Set
resp~ B = ∀ {a a'} → El~ reflU a a' → U~ (B a) (B a')

data U where
  ℕ' : U
  Π' : (A : U)(B : El A → U) → resp~ B → U

U~ ℕ'         ℕ'           = ⊤
U~ ℕ'         (Π' _ _ _)   = ⊥
U~ (Π' _ _ _) ℕ'           = ⊥
U~ (Π' A B _) (Π' A' B' _) = Σ (U~ A A') λ A~ → ∀ {a a'} → El~ A~ a a' → U~ (B a) (B' a')

reflU {ℕ'}        = tt
reflU {Π' A B Br} = reflU , λ a~ → Br a~

El ℕ'         = ℕ
El (Π' A B _) = (a : El A) → El (B a)

El~ {ℕ'}       {ℕ'}         A~        x y = x ≡ y
El~ {Π' A B _} {Π' A' B' _} (A~ , B~) f g = ∀ {a a'} a~ → El~ (B~ a~) (f a) (g a')

Here U itself is equipped with a relation and each El type is also equipped with a heterogeneous equivalence. The resp~ field in the type of Π' requires that the codomain type respects the chosen equivalences.

This definition, however, is not covered by any specification of induction-recursion in the literature. In classic IR, an inductive sort can be fibered over an external type. Here, U~ maps from two copies of U to Set; hence the name "double induction-recursion". More generally, Agda supports recursive functions mapping out from any telescope of inductive sorts.

In this specific example, the double IR can be avoided by defining U~ inductively and El~ homogeneously, but a) that doesn't compute as strictly as we'd like to have in observational TT b) in the complete formalization of the setoid universe we'll need double IR anyway in some other places.

In the recent OTT paper, Pujet & Tabareau use similar IR for the semantics of the universe. They work in constructive set theory and don't give a particular justification for this IR. I don't know enough about set theory to tell if this IR is indeed trivially valid there. However, I think that double IR is very likely to make sense and it is the most convenient way to formalize setoid universes. The alternative is rather gnarly: Altenkirch et al. defines the same setoid universe without IR, using complicated induction-induction.

Endo-induction-recursion

In classic IR, a recursive function has to map into an external type, i. e. some type which is not declared as a sort in the signature that is being defined. In Agda, we can map wherever we want. Example:

data A : Set
data B : A → Set
f      : (a : A) → B a
data A where ...
data B where ...

This is again not described in the literature. But the semantics looks a bit easier in this case, as far as I see. I expect that endo-IR can be derived from quotient induction and UIP. The following is due to Ambrus Kaposi.

First, we define a quotient inductive type which includes f as an ordinary constructor and the definition of f as a bunch of quotient equations. Then, we use elimination to define f again as a function instead, which is always possible if the original f specification is properly structurally recursive. The thus strictified initial algebra can be then shown to be equivalent to the one with the quotienting.

The point is that we can often redefine quotients as functions, which is more convenient in formalization. This is useful even if we can't easily get rid of all quotienting. Endo-IR can be viewed as a shortcut to such strictification which relies on Agda's termination checking.

3. Summary of Agda features in the literature

---

I describe sets of features which are covered in the literature. These are the largest such sets that I was able to find.

• Chapter 5 of my thesis specifies infinitary inductive-inductive types. It's a special case of quotient induction-induction, but quotients can be trivially dropped from the syntax & the semantics. This chapter allows us to compute eliminators and their beta rules in pretty much the same way as they would appear in Agda. Prop is not supported though, nor sorts at different universe levels; Section 5.6 only supports having the same universe level for all sorts. I skipped this feature because universe levels are rather tedious to wrestle all the time.
• This note of mine extends this to infinitary induction-induction-recursion. This follows the style of Dybjer & Setzer, in that recursive functions eliminate from exactly one inductive sort to an external type. Semantics is not developed in the note but I don't expect any complication for the set-truncated case.
• As I mentioned, Johan & Polonsky cover most ground from nested induction.
• Evan Cavallo covers most ground from higher inductive types in the cubical mode. It's a different cubical type theory, but everything should be straightforward to port over to Agda's flavor.

I shall leave coinduction to someone else as I'm not that familiar with the literature.