Recursive Data Type - Theory

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

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 (thus represented by the unit type) and Succ takes another Nat (thus another element of ).

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.

Read more about this topic:  Recursive Data Type

Famous quotes containing the word theory:

    “The theory seems to be that so long as a man is a failure he is one of God’s chillun, but that as soon as he has any luck he owes it to the Devil.”
    —H.L. (Henry Lewis)

    “The human species, according to the best theory I can form of it, is composed of two distinct races, the men who borrow and the men who lend.”
    —Charles Lamb (1775–1834)

    “The struggle for existence holds as much in the intellectual as in the physical world. A theory is a species of thinking, and its right to exist is coextensive with its power of resisting extinction by its rivals.”
    —Thomas Henry Huxley (1825–95)