- Recursive type
In computer

programming language s, a**recursive type**is adata type for values that may contain other values of the same type.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:

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 a empty rest of the list).

**Theory**In

type theory , a recursive type has the general form μα.T wherethetype variable α may appear in the type T and stands for theentire type itself.For example, the natural number (see

Peano arithmetic ) maybe defined by the Haskell datatype:data Nat = Zero | Succ NatIn type theory, we would say: $nat\; =\; mu\; alpha.\; 1\; +\; alpha$ where the two arms of the

sum type representthe Zero and Succ data constructors. Zero takes no arguments(thus represented by theunit type ) and Succ takes anotherNat (thus another element of $mu\; alpha.\; 1\; +\; alpha$).There are two forms of recursive types: the so-called isorecursivetypes, and equirecursive types. The two forms differ in howterms of a recursive type are introduced and eliminated.

**Isorecursive types**With isorecursive types, the recursive type $mu\; alpha\; .\; T$ and its expansion (or "unrolling") $T\; [mu\; alpha.T\; /\; alpha]$ are distinct (and disjoint) types with special term constructs, usually called "roll" and "unroll", that form an

isomorphism between them. To be precise: $roll\; :\; T\; [mualpha.T/alpha]\; o\; mualpha.T$ and $unroll\; :\; mualpha.T\; o\; T\; [mualpha.T/alpha]$, and these two areinverse function s.**In type synonyms**Recursion is not allowed in

type synonym s in Miranda,OCaml (unless -rectypes flag is used), and Haskell; so for example the following Haskell types are illegal:type Bad = (Int, Bad)type Evil = Bool -> EvilInstead, you must wrap it inside an algebraic data type (even if it only has one constructor):

data Good = Pair Int Gooddata Fine = Fun (Bool->Fine)This is because type synonyms, like

typedef s 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. (i.e. "Bad" will grow indefinitely: (Int, (Int, (Int, ... Bad))...) )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".

**Equirecursive types**Under equirecursive rules, a recursive type $mu\; alpha\; .\; T$ and its unrolling $T\; [mualpha.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.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.Infunctional programming languages, isorecursive types (in the guise of datatypes) are far more ubiquitous.**See also***

Recursion

*Algebraic data type

*Wikimedia Foundation.
2010.*

### Look at other dictionaries:

**Type system**— Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing … Wikipedia**Recursive categorical syntax**— Recursive categorical syntax, also sometimes called algebraic syntax, is an algebraic theory of syntax developed by Michael Brame as an alternative to transformational generative grammar. It is a type of dependency grammar, and is related to link … Wikipedia**Type recursif**— Type récursif Dans un langage de programmation, un type récursif ou type inductif est un type de données pour des valeurs qui contiennent d autres valeurs du même type. Un exemple est le type liste en Haskell : data List a = Nil | Cons a… … Wikipédia en Français**Recursive language**— This article is about a class of formal languages as they are studied in mathematics and theoretical computer science. For computer languages that allow a function to call itself recursively, see Recursion (computer science). In mathematics,… … Wikipedia**Recursive set**— In computability theory, a set of natural numbers is called recursive, computable or decidable if there is an algorithm which terminates after a finite amount of time and correctly decides whether or not a given number belongs to the set. A more… … Wikipedia**Recursive languages and sets**— This article is a temporary experiment to see whether it is feasible and desirable to merge the articles Recursive set, Recursive language, Decidable language, Decidable problem and Undecidable problem. Input on how best to do this is very much… … Wikipedia**Recursive ordinal**— In mathematics, specifically set theory, an ordinal α is said to be recursive if there is a recursive binary relation R that well orders a subset of the natural numbers and the order type of that ordering is α. It is trivial to check that ω is… … Wikipedia**Recursive filter**— In signal processing, a recursive filter is a type of filter which re uses one or more of its outputs as an input. This feedback typically results in an unending impulse response (commonly referred to as infinite impulse response (IIR)),… … Wikipedia**Type statique**— Typage statique Sommaire 1 Définition 2 Langages à objets et typage statique 3 Problèmes 4 Résolution, autres difficultés … Wikipédia en Français**Type récursif**— Dans un langage de programmation, un type récursif ou type inductif est un type de données pour des valeurs qui contiennent d autres valeurs du même type. Cette notion s applique naturellement dans l étude des listes et des arbres. Sommaire 1… … Wikipédia en Français