Inductive type

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. Inductive types usually come with a function to prove properties about them. Thus, "nat" may come with (in Coq syntax): nat_elim : (forall P : nat -> Prop, (P 0) -> (forall n, P n -> P (S n)) -> (forall n, P n)). In words: for any proposition "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 are well-founded types in intuitionistic type theory (ITT). They generalize natural numbers, lists, binary trees, and other "tree-shaped" data types. Let be a universe of types. Given a type : and a dependent family : → , one can form a W-type . The type may be thought of as "labels" for the (potentially infinitely many) constructors of the inductive type being defined, whereas 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 elements : and where the node labeled by has ()-many subtrees.