Recursive type

From Wikipedia, the free encyclopedia

In computer programming languages, a recursive type is a data 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").

Recursion is not allowed in Miranda or Haskell synonym types, so the following Haskell types are illegal:

type Bad = (Int, Bad)
type Evil = Bool -> Evil

Inversely, the seemingly equivalent algebraic data types are acceptable:

data Good = Pair Int Good
data Fine = Fun (Bool->Fine)

Contents 1 Theory 1.1 Isorecursive types 1.2 Equirecursive types 2 See also

[edit] 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 number (see Peano arithmetic) may be defined by the Haskell datatype:

  data Nat = Zero | Succ Nat

And in type theory we would say nat = μα.1 + α. Where the two arms of the sum type represent the Zero and Succ data constructors, with Zero taking no arguments (thus represented by the unit type), and Succ taking another Nat (thus another element of μα.1 + α).

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.

[edit] Isorecursive types

With isorecursive types, the recursive type μα.T and its expansion (or unrolling) T[μα.T / α] are distinct (and disjoint) 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.

[edit] Equirecursive types

Under equirecursive rules, a recursive type μα.T and its unrolling T[μα.T / α] 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. In functional programming languages, isorecursive types (in the guise of datatypes) are far more ubiquitous.

[edit] See also

• Recursion
• Algebraic data type

This article was originally based on material from the Free On-line Dictionary of Computing, which is licensed under the GFDL.