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.
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
Please expand.
Please expand.
Please expand.
The 'standard' denotational semantics of recursive types is given through domain theory.
The idea is to see the recursive definition as a functor on domains. If this is sufficiently well-behaved, then it has a fixed point . When using information systems this can be made into a strict equality 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 using the relation on its unfolding , 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
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.
Barendregt, Henk, Wil Dekkers, and Richard Statman. 2013. Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press. https://doi.org/10.1017/CBO9781139032636.
@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}
}
Pitts, Andrew M. 1996. ‘Relational Properties of Domains’. Information and Computation 127 (2): 66–90. https://doi.org/10.1006/inco.1996.0052. [pdf]
@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}
}