This articleneeds additional citations forverification. Please helpimprove this article byadding citations to reliable sources. Unsourced material may be challenged and removed. Find sources: "Inductive type" – news ·newspapers ·books ·scholar ·JSTOR(January 2018) (Learn how and when to remove this message)

Intype theory, a system hasinductive types if it has facilities for creating a new type from constants and functions that create terms of that type. The feature serves a role similar todata structures in a programming language and allows a type theory to add concepts likenumbers,relations, andtrees. As the name suggests, inductive types can be self-referential, but usually only in a way that permitsstructural recursion.

The standard example is encoding thenatural numbers usingPeano's encoding. It can be defined inRocq (previously known asCoq) as follows:

Inductivenat:Type:=|0:nat|S:nat->nat.

Here, a natural number is created either from the constant "0" or by applying the function "S" to another natural number. "S" is thesuccessor function which represents adding 1 to a number. Thus, "0" is zero, "S 0" is one, "S (S 0)" is two, "S (S (S 0))" is three, and so on.

Since their introduction, inductive types have been extended to encode more and more structures, while still beingpredicative and supporting structural recursion.

Inductive types usually come with a function to prove properties about them. Thus, "nat" may come with (in Rocq syntax):

nat_elim:(forallP:nat->Prop,(P0)->(foralln,Pn->P(Sn))->(foralln,Pn)).

In words: for any predicate "P" over natural numbers, given a proof of "P 0" and a proof of "P n -> P (n+1)", we get back a proof of "forall n, P n". This is the familiar induction principle for natural numbers.

W-types arewell-founded types inintuitionistic type theory (ITT).^[1] They generalize natural numbers, lists, binary trees, and other "tree-shaped" data types. LetU be auniverse of types. Given a typeA :U and adependent familyB :A →U, one can form a W-type${\displaystyle {\mathsf{W}}_{a:A}B(a)}$. The typeA may be thought of as "labels" for the (potentially infinitely many) constructors of the inductive type being defined, whereasB indicates the (potentially infinite)arity of each constructor. W-types (resp. M-types) may also be understood as well-founded (resp. non-well-founded) trees with nodes labeled by elementsa :A and where the node labeled bya hasB(a)-many subtrees.^[2] Each W-type is isomorphic to the initial algebra of a so-calledpolynomial functor.

Let0,1,2, etc. be finite types with inhabitants 1₁ :1, 1₂, 2₂:2, etc. One may define the natural numbers as the W-type$${\displaystyle \mathbb{N}:={\mathsf{W}}_{x:\mathbf{2}}f(x)}$$withf :2 →U is defined byf(1₂) =0 (representing the constructor for zero, which takes no arguments), andf(2₂) =1 (representing the successor function, which takes one argument).

One may define lists over a typeA :U as${\displaystyle \mathrm{List}(A):={\mathsf{W}}_{(x:\mathbf{1}+A)}f(x)}$ whereand 1₁ is the sole inhabitant of1. The value of${\displaystyle f(\mathrm{inl}(1_{\mathbf{1}}))}$ corresponds to the constructor for the empty list, whereas the value of${\displaystyle f(\mathrm{inr}(a))}$ corresponds to the constructor that appendsa to the beginning of another list.

The constructor for elements of a generic W-type${\displaystyle {\mathsf{W}}_{x:A}B(x)}$ has type$${\displaystyle \mathsf{s}\mathsf{u}\mathsf{p}:\prod _{a:A}(B(a)\to {\mathsf{W}}_{x:A}B(x))\to {\mathsf{W}}_{x:A}B(x).}$$We can also write this rule in the style of anatural deduction proof,$${\displaystyle \frac{a:Af:B(a)\to {\mathsf{W}}_{x:A}B(x)}{\mathsf{s}\mathsf{u}\mathsf{p}(a,f):{\mathsf{W}}_{x:A}B(x)}.}$$

The elimination rule for W-types works similarly tostructural induction on trees. If, whenever a property (under thepropositions-as-types interpretation)${\displaystyle C:{\mathsf{W}}_{x:A}B(x)\to U}$ holds for all subtrees of a given tree it also holds for that tree, then it holds for all trees.

$${\displaystyle \frac{w:{\mathsf{W}}_{a:A}B(a)a:A,f:B(a)\to {\mathsf{W}}_{x:A}B(x),c:\prod _{b:B(a)}C(f(b))⊢h(a,f,c):C(\mathsf{s}\mathsf{u}\mathsf{p}(a,f))}{\mathsf{e}\mathsf{l}\mathsf{i}\mathsf{m}(w,h):C(w)}}$$

In extensional type theories, W-types (resp. M-types) can be defined up toisomorphism asinitial algebras (resp. final coalgebras) forpolynomial functors. In this case, the property of initiality (res. finality) corresponds directly to the appropriate induction principle.^[3] In intensional type theories with theunivalence axiom, this correspondence holds up to homotopy (propositional equality).^[4][5][6]

M-types aredual to W-types, and representcoinductive (potentially infinite) data such asstreams.^[7] M-types can be derived from W-types.^[8]

This technique allowssome definitions of multiple types that depend on each other. For example, defining twoparity predicates onnatural numbers using two mutually inductive types in Rocq:

Inductiveeven:nat->Prop:=|zero_is_even:evenO|S_of_odd_is_even:(foralln:nat,oddn->even(Sn))withodd:nat->Prop:=|S_of_even_is_odd:(foralln:nat,evenn->odd(Sn)).

Induction-recursion started as a study into the limits of ITT. Once found, the limits were turned into rules that allowed defining new inductive types. These types could depend upon a function and the function on the type, as long as both were defined simultaneously.

Universe types can be defined using induction-recursion.

Induction-induction allows definition of a type and a family of types at the same time. So, a typeA and a family of types${\displaystyle B:A\to Type}$.

This is a current research area inHomotopy Type Theory (HoTT). HoTT differs from ITT by its identity type (equality). Higher inductive types not only define a new type with constants and functions that create elements of the type, but also new instances of the identity type that relate them.

A simple example is thecircle type, which is defined with two constructors, a basepoint;

base :circle

and a loop;

loop :base =base.

The existence of a new constructor for the identity type makescircle a higher inductive type.

• Coinduction permits (effectively) infinite structures in type theory.

• Univalent Foundations Program (2013).Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.

• Induction-Recursion Slides
• Induction-Induction Slides
• Higher Inductive Types: a tour of the menagerie

• Type theory

• Articles needing additional references from January 2018
• All articles needing additional references