Inductive Type

Idea

In type theory, an inductive type is a type specified by constructors, together with elimination and computation rules, expressing that functions and proofs out of the type are defined by structural recursion or induction on those constructors.

Inductive types support:

• constructors, which generate elements of the type
• recursion, which defines functions out of the type by specifying their action on constructors
• induction, which proves properties of all elements by considering the constructors

They are closely related to well-foundedness, since inductive data is built in finitely many steps, with no infinite descending process of construction.

Signature

An inductive type signature $\Sigma$ consists of:

• A sort symbol $\dot{A}$
• For each $i\in [m]$, a strictly positive telescope ${\Phi }_i[\dot{A}]$

From this signature, one generates point constructors for a type $A$ by,

$$c_i:{\Phi }_i[A]\to A$$

Algebras

An algebra for an inductive type signature $\Sigma$ consists of a carrier $A$ together with, for each point constructor arity ${\Phi }_i[-]$, a function

$$c_i:{\Phi }_i[A]\to A.$$

These operations extend to interpretations of all formal terms built from the constructors.

The arities ${\Phi }_i$ usually assemble into a functor

$$\begin{array}{rl}& S_{\Sigma }:\mathrm{Type}\to \mathrm{Type}\\ & S_{\Sigma }(X)=\sum _i{\Phi }_i[X],\end{array}$$

An $S_{\Sigma }$-algebra is a pair $(A,\alpha )$ where $A$ is an object and

$$\alpha :S_{\Sigma }(A)\to A.$$

Semantically, an inductive type is given by the carrier of an initial $S_{\Sigma }$-algebra $(\mu S_{\Sigma },\mathrm{in})$:

$$\mathsf{in}:S_{\Sigma }(\mu S_{\Sigma })\to \mu S_{\Sigma }.$$

Initiality means that for any other $S_{\Sigma }$-algebra

$$\alpha :S_{\Sigma }(A)\to A,$$

there exists a unique algebra morphism

$${\mathsf{rec}}_{\alpha }:\mu S_{\Sigma }\to A$$

such that

$${\mathsf{rec}}_{\alpha }\circ \mathsf{in}=\alpha \circ S_{\Sigma }({\mathsf{rec}}_{\alpha }).$$

This universal property explains:

• recursion, by existence of ${\mathsf{rec}}_{\alpha }$
• uniqueness of recursive definitions, by uniqueness of the algebra morphism
• computation rules, by commutativity of the defining diagram

In extensional type theory, this matches the usual induction principle closely. In HoTT, the corresponding notion is usually a homotopy-initial algebra.

Type-theoretic Presentation

In type theory, inductive types are usually introduced by formation, introduction, elimination, and computation rules.

Using Agda-inspired syntax, a schematic declaration has the form:

$$\begin{array}{rl}& \mathsf{data}A:\mathcal{U}\mathsf{where}\\ & {\mathsf{c}}_1:{\Phi }_1\to A\\ & ⋮\\ & {\mathsf{c}}_n:{\Phi }_n\to A\end{array}$$

where the telescopes ${\Phi }_i$ may refer to $A$ only in strictly positive positions.

Example: natural numbers

The natural numbers are generated by two constructors:

$$\frac{}{\Gamma ⊢\mathbb{N}:\mathcal{U}}\frac{}{\Gamma ⊢\mathsf{zero}:\mathbb{N}}\frac{\Gamma ⊢n:\mathbb{N}}{\Gamma ⊢\mathsf{suc}(n):\mathbb{N}}$$

The induction principle (eliminator) is:

$$\frac{\Gamma ,n:\mathbb{N}⊢P(n):\mathcal{U}\Gamma ⊢c_0:P(\mathsf{zero})\Gamma ⊢c_s:{\prod }_{n:\mathbb{N}}P(n)\to P(\mathsf{suc}(n))}{\Gamma ⊢{\mathsf{elim}}_{\mathbb{N}}(c_0,c_s):{\prod }_{n:\mathbb{N}}P(n)}$$

with computation rules:

$$\begin{array}{rl}{\mathsf{elim}}_{\mathbb{N}}(c_0,c_s,\mathsf{zero})& \equiv c_0\\ {\mathsf{elim}}_{\mathbb{N}}(c_0,c_s,\mathsf{suc}(n))& \equiv c_s(n,{\mathsf{elim}}_{\mathbb{N}}(c_0,c_s,n)).\end{array}$$

This expresses the usual fact that to define a function or prove a property on $\mathbb{N}$, it is enough to handle the constructors.

Strict positivity

The recursive occurrences of an inductive type must appear only in strictly positive positions.

Intuitively, this means the type being defined may appear as an argument to constructors, but not to the left of a function arrow in a way that would make the definition contravariant.

Strict positivity is needed to ensure that the definition behaves like a genuine inductive construction. If it is dropped, one can lose normalization, logical consistency, or the existence of well-behaved initial algebra semantics.

For this reason, proof assistants such as Agda and Coq impose positivity checks on inductive definitions.

Universe-based presentation of strictly positive types

One convenient way to describe a class of strictly positive inductive types is via a universe of codes for functors, together with a least fixed-point operator.

This gives a generic representation of many strictly positive inductive types. It is a useful encoding, but it is not the only way to present inductive types.

Relation with W-types

W-types provide the initial algebras for polynomial functors, and many ordinary inductive types can be represented in terms of them. Because of this, W-types are often used as the canonical semantic model of inductive types in dependent type theory.

However, not every inductive type should be identified outright with tree structure. While trees are often the right semantic intuition, the general notion is more cleanly captured by constructors, induction, and initiality.

See also

• W Type
• Strictly Positive Type
• Initial Algebra
• Polynomial Functor
• Inductive Family
• Inductive-Inductive Type
• Quotient Inductive Type
• Tarski Universe
• Fixed Point

References

• forsberg2013-inductive-inductive-thesis
• dybjer1999-inductive-recursive
• kaposi2019-finitary-induction-induction