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).
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.
With isorecursive types, the recursive type and its expansion (or unrolling) 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.
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. (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.
Under equirecursive rules, a recursive type and its unrolling 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.