In computer programming languages, a recursive data type (also known as a recursively-defined, inductively-defined or inductive 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. Contents 1 Example 1.1 Mutually recursive data types 2 Theory 2.1 Isorecursive types 2.2 Equirecursive types 2.2.1 In type synonyms 3 See also 4 Notes Example[edit] See also: Recursion (computer science) § Recursive data structures (structural recursion) 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<E> E value; List<E> next; 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[edit]
Further information:
f: [t[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 [t[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:[1] datatype 'a tree = Empty Node of 'a * 'a forest and 'a forest = Nil Cons of 'a tree * 'a forest Theory[edit] 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 (see Peano arithmetic) may be defined by the Haskell datatype: data Nat = Zero Succ Nat In type theory, we would say: n a t = μ α .1 + α displaystyle nat=mu alpha .1+alpha where the two arms of the sum type 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 μ α .1 + α displaystyle mu alpha .1+alpha ). 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[edit] With isorecursive types, the recursive type μ α . T displaystyle mu alpha .T and its expansion (or unrolling) T [ μ α . T / α ] displaystyle T[mu alpha .T/alpha ] (Where the notation X [ Y / Z ] displaystyle X[Y/Z] 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. To be precise: r o l l : T [ μ α . T / α ] → μ α . T displaystyle roll:T[mu alpha .T/alpha ]to mu alpha .T and u n r o l l : μ α . T → T [ μ α . T / α ] displaystyle unroll:mu alpha .Tto T[mu alpha .T/alpha ] , and these two are inverse functions. Equirecursive types[edit] Under equirecursive rules, a recursive type μ α . T displaystyle mu alpha .T and its unrolling T [ μ α . T / α ] displaystyle T[mu alpha .T/alpha ] 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 stipulate 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(n
log n) time, which can easily be compared.[2]
Equirecursive types capture the form of self-referential (or mutually
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 (in the guise of datatypes) are far more common.
In type synonyms[edit]
Recursion is not allowed in type synonyms in Miranda,
type Bad = (Int, Bad) type Evil = Bool -> Evil Instead, you must wrap it inside an algebraic data type (even if it only has one constructor): data Good = Pair Int Good data Fine = Fun (Bool->Fine) This is because type synonyms, like typedefs in C, are replaced with their definition at compile time. (Type synonyms are not "real" types; they are just "aliases" for convenience of the programmer.) 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: (Int, (Int, (Int, ... . 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. See also[edit] Recursive definition Algebraic data type Node (computer science) Notes[edit] ^ Harper 2000, "Data Types". ^ "Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types". v t e Data types Uninterpreted Bit
Byte
Trit
Tryte
Word
Numeric Arbitrary-precision or bignum Complex Decimal Fixed point Floating point Double precision Extended precision Half precision Long double Minifloat Octuple precision Quadruple precision Single precision Integer signedness Interval Rational Pointer Address physical virtual Reference Text Character String null-terminated Composite Algebraic data type generalized Array Associative array Class Dependent Equality Inductive List Object metaobject Option type Product Record Set Union tagged Other Boolean Bottom type Collection Enumerated type Exception Function type Opaque data type Recursive data type Semaphore Stream Top type Type class Unit type Void Related topics Abstract data type Data structure Generic Kind metaclass Parametric polymorphism Primitive data type Protocol interface Subtyping Type constructor Type conversion Type system Type theory See also platform-dependent and independent units of information This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, ver |