Data of recursive types are usually viewed as directed graphs[citation needed].
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.
Data types can also be defined by mutual recursion.
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 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.
For example, the natural numbers (see Peano arithmetic) may be defined by the Haskell datatype: In type theory, we would say:
where the two arms of the sum type represent the Zero and Succ data constructors.
The two forms differ in how terms of a recursive type are introduced and eliminated.
indicates that all instances of Z are replaced with Y in X) are distinct (and disjoint) types with special term constructs, usually called roll and unroll, that form an isomorphism between them.
Since direct comparison does not make sense on an equirecursive type, they can be converted into a canonical form in O(n log n) time, which can easily be compared.
[2] Isorecursive types capture the form of self-referential (or mutually referential) type definitions seen in nominal object-oriented programming languages, and also arise in type-theoretic semantics of objects and classes.
In functional programming languages, isorecursive types (in the guise of datatypes) are common too.
Another way to see it is that a level of indirection (the algebraic data type) is required to allow the isorecursive type system to figure out when to roll and unroll.