Inductive type

This article needs additional citations for verification. Please help improve this article by adding 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)

In type theory, a system has inductive 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 to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.

The standard example is encoding the natural numbers using Peano's encoding. It can be defined in Coq as follows:

 Inductive nat : 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 the successor 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 being predicative and supporting structural recursion.