In computer
programming language
A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language.
The description of a programming ...
s, a recursive data type (also known as a recursively-defined, inductively-defined or inductive data type) is a
data type
In computer science and computer programming, a data type (or simply type) is a set of possible values and a set of allowed operations on it. A data type tells the compiler or interpreter how the programmer intends to use the data. Most progra ...
for values that may contain other values of the same type. Data of recursive types are usually viewed as
directed graphs.
An important application of recursion in computer science is in defining dynamic data structures such as Lists and Trees. Recursive data structures can dynamically grow to an arbitrarily large size in response to runtime requirements; in contrast, a static array's size requirements must be set at compile time.
Sometimes the term "inductive data type" is used for
algebraic data types which are not necessarily recursive.
Example
An example is the
list type, in
Haskell:
data List a = Nil , Cons a (List a)
This indicates that a list of a's is either an empty list or a cons cell containing an 'a' (the "head" of the list) and another list (the "tail").
Another example is a similar singly linked type in Java:
class List
This indicates that non-empty list of type E contains a data member of type E, and a reference to another List object for the rest of the list (or a null reference to indicate that this is the end of the list).
Mutually recursive data types
Data types can also be defined by
mutual recursion. The most important basic example of this is a
tree
In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, including only woody plants with secondary growth, plants that are ...
, which can be defined mutually recursively in terms of a forest (a list of trees). Symbolically:
f:
[1 ..., t[k">[1.html" ;"title="[1">[1 ..., t[k
t: v f
A forest ''f'' consists of a list of trees, while a tree ''t'' consists of a pair of a value ''v'' and a forest ''f'' (its children). This definition is elegant and easy to work with abstractly (such as when proving theorems about properties of trees), as it expresses a tree in simple terms: a list of one type, and a pair of two types.
This mutually recursive definition can be converted to a singly recursive definition by inlining the definition of a forest:
t: v
[1 ..., t[k">[1.html" ;"title="[1">[1 ..., t[k
A tree ''t'' consists of a pair of a value ''v'' and a list of trees (its children). This definition is more compact, but somewhat messier: a tree consists of a pair of one type and a list another, which require disentangling to prove results about.
In Standard ML, the tree and forest data types can be mutually recursively defined as follows, allowing empty trees:
datatype 'a tree = Empty , Node of 'a * 'a forest
and 'a forest = Nil , Cons of 'a tree * 'a forest
In Haskell, the tree and forest data types can be defined similarly:
data Tree a = Empty
, Node (a, Forest a)
data Forest a = Nil
, Cons (Tree a) (Forest a)
Theory
In
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundat ...
, a recursive type has the general form μα.T where the
type variable In type theory and programming languages, a type variable is a mathematical variable ranging over types. Even in programming languages that allow mutable variables, a type variable remains an abstraction, in the sense that it does not correspond t ...
α may appear in the type T and stands for the entire type itself.
For example, the natural numbers (see
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
) may be defined by the Haskell datatype:
data Nat = Zero , Succ Nat
In type theory, we would say:
where the two arms of the
sum type
In computer science, a tagged union, also called a variant, variant record, choice type, discriminated union, disjoint union, sum type or coproduct, is a data structure used to hold a value that could take on several different, but fixed, types. O ...
represent the Zero and Succ data constructors. Zero takes no arguments (thus represented by the
unit type) and Succ takes another Nat (thus another element of
).
There are two forms of recursive types: the so-called isorecursive types, and equirecursive types. The two forms differ in how terms of a recursive type are introduced and eliminated.
Isorecursive types
With isorecursive types, the recursive type
and its expansion (or ''unrolling'')