Recursive Types

A programming language supports recursive types if it is able to express data types which are defined in terms of themselves. Unlike inductive types, the position of the 'recursive call' is completely unrestricted.

In functional languages, recursive types are usually supported through the ability to have 'recursive calls' when defining an algebraic data type.

In imperative languages, recursive types are usually implemented through the use of pointers.

Type isomorphisms

Consider, for example, the natural numbers as an algebraic data type. In Haskell:

data Nat = Zero | Succ Nat

That is: every natural number is either zero, or the successor of another natural number. This data type can be (slightly informally) encoded by the recursive type equation

X \cong \mathbf{1} + X

Please expand.

Equirecursive presentation

Please expand.

Isorecursive presentation

Please expand.

Denotational semantics

The 'standard' denotational semantics of recursive types is given through domain theory.

The idea is to see the recursive definition \text{rec}\ X. F(X) as a functor F on domains. If this F is sufficiently well-behaved, then it has a fixed point D \cong F(D). When using information systems this can be made into a strict equality D = F(D) as well.

The adequacy of such a semantics with respect to syntax is a difficult problem. The reason is that defining logical relations is not obvious. The 'obvious' way would be to try to define the relation at \text{rec}\ X. F(X) using the relation on its unfolding F(\text{rec}\ X. F(X)), which is not inductive. A solution is given by Pitts' minimal invariants Pitts 1995.

For more information, see the main article on recursive domain equations

See also

• Recursive domain equations
• Plotkin's Fixed Point Calculus (FPC)
• Strict positivity

References

• FPC originates in Plotkin 1985. See also the books by Gunter, and possibly Winskel.

• A thorough review of systems of equirecursive types in Curry-style is given in Part II of the following book, which has been coauthored with Mario Coppo and Felice Cardone.

@book{barendregt_lambda_2013,
	series = {Perspectives in {Logic}},
	title = {Lambda {Calculus} with {Types}},
	publisher = {Cambridge University Press},
	author = {Barendregt, Henk and Dekkers, Wil and Statman, Richard},
	year = {2013},
	doi = {10.1017/CBO9781139032636}
}

• Adequacy for recursive types can be proven through Pitts' minimal invariants:

@article{pitts_1996,
	title = {Relational Properties of Domains},
	volume = {127},
	doi = {10.1006/inco.1996.0052},
	pages = {66--90},
	number = {2},
	journaltitle = {Information and Computation},
	author = {Pitts, Andrew M.},
	date = {1996}
}