In computer programming languages, a recursive data type is a data type 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
This indicates that a list of a's is either an empty list or a cons cell containing an 'a' and another list. 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.
Data types can also be defined by mutual recursion. The most important basic example of this is a tree, which can be defined mutually recursively in terms of a forest. Symbolically: f: ,..., t,..., tk A tree t consists of a pair of [a value v and a list of trees. 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 data Forest a = Nil | Cons
Theory
In type theory, a recursive type has the general form μα.T where the type variable α may appear in the type T and stands for the entire type itself. For example, the natural numbers 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 represent the Zero and Succ data constructors. Zero takes no arguments and Succ takes another Nat. 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 are distinct types with special term constructs, usually called roll and unroll, that form an isomorphism between them. To be precise: and, and these two are inverse functions.
Equirecursive types
Under equirecursive rules, a recursive type and its unrolling are equal -- that is, those two type expressions are understood to denote the same type. In fact, most theories of equirecursive types go further and essentially specify that any two type expressions with the same "infinite expansion" are equivalent. As a result of these rules, equirecursive types contribute significantly more complexity to a type system than isorecursive types do. Algorithmic problems such as type checking and type inference are more difficult for equirecursive types as well. Since direct comparison does not make sense on an equirecursive type, they can be converted into a canonical form in O time, which can easily be compared. Equirecursive types capture the form of self-referential type definitions seen in procedural and object-oriented programming languages, and also arise in type-theoretic semantics of objects and classes. In functional programming languages, isorecursive types are far more common.
In type synonyms
Recursion is not allowed in type synonyms in Miranda, OCaml, and Haskell; so for example the following Haskell types are illegal: type Bad = type Evil = Bool -> Evil
Instead, you must wrap it inside an algebraic data type : data Good = Pair Int Good data Fine = Fun
This is because type synonyms, like typedefs in C, are replaced with their definition at compile time. But if you try to do this with a recursive type, it will loop infinitely because no matter how many times you substitute it, it still refers to itself, e.g. "Bad" will grow indefinitely: Bad → → → .... Another way to see it is that a level of indirection is required to allow the isorecursive type system to figure out when to roll and unroll.
