A recursive type is defined in terms of itself, allowing values with unbounded finite structure.

A list of elements of type $A$ can be described by the equation

$$\text{List}(A) \cong 1 + A\times \text{List}(A),$$

where $1$ is a one-value unit type whose sole value represents the empty-list case, and the product represents a head together with another list.

In constructor notation:

List(A) = Nil | Cons(A, List(A))

A finite list such as [2, 5] becomes

Cons(2, Cons(5, Nil))

The recursive reference does not mean a value physically contains an infinite list. Each constructor contributes one finite layer, and recursion allows another layer to follow.

Trees are defined similarly. For example,

$$\text{Tree}(A) \cong 1 + A\times\text{Tree}(A)\times\text{Tree}(A).$$

Types built from named constructors, products, sums and recursion are commonly called algebraic data types. Their constructor structure gives a natural form for recursive functions and structural-induction proofs: one program or proof case corresponds to each constructor.

Recursive types connect data representation, recursion, pattern matching and inductive reasoning in one reusable abstraction.