Recursive Types
How do you write the type of a linked list? A list of numbers is either empty, or a number paired with
another list of numbers. The type refers to itself. With
records and variants
alone we can only build types of finite depth; to name a self-referential structure we need a new
binder, \mu ("mu"), that ties the knot:
\mathsf{NatList} \;=\; \mu X.\ \langle\, \mathsf{nil}:\mathsf{Unit},\ \mathsf{cons}:\{\mathsf{head}:\mathsf{Nat},\ \mathsf{tail}:X\}\,\rangle.
The type variable X stands for "the whole type again", and
\mu X.\,T is the type X such that
X = T. Read the equation above as: a
\mathsf{NatList} is a variant — \mathsf{nil}, or a
\mathsf{cons} record whose \mathsf{tail} is once
more a \mathsf{NatList}. Recursive types are what let a finite piece of syntax
describe an unboundedly deep structure — lists, trees, streams, JSON, the syntax trees of the very
languages we are studying.
The defining isomorphism: fold and unfold
The meaning of \mu is one equation — a recursive type is
isomorphic to its own one-step unfolding, the body with the recursive type plugged back in for
X:
\mu X.\,T \;\;\cong\;\; T[\,\mu X.\,T \,/\, X\,].
The two directions of that isomorphism are named. \mathsf{unfold}
exposes one layer of structure; \mathsf{fold} packs it back
up. They are mutually inverse:
\mathsf{unfold}:\ \mu X.\,T \;\to\; T[\mu X.\,T/X]
\qquad
\mathsf{fold}:\ T[\mu X.\,T/X] \;\to\; \mu X.\,T.
This is the iso-recursive discipline: the two types are not literally equal,
but there is an explicit coercion each way, and every program must say \mathsf{fold}
to build a recursive value and \mathsf{unfold} to inspect one. It keeps type
checking trivially syntax-directed — the checker never has to decide whether two cyclic types are the
same, because you told it exactly where the knot is tied.
Iso-recursive vs equi-recursive
There are two design choices for how recursive types relate to their unfoldings, and every real language
picks one.
-
Iso-recursive — \mu X.\,T and its unfolding are
isomorphic, connected by explicit \mathsf{fold}/\mathsf{unfold}
coercions the programmer writes (ML's datatype constructors and pattern-matches insert these for
you). Type checking stays simple and syntax-directed.
-
Equi-recursive — \mu X.\,T and its unfolding are
literally the same type, silently interchangeable. More convenient to use, but the type
checker must now decide equality of two potentially infinite regular trees, which requires
a coinductive algorithm (compare lazily, remembering pairs already assumed equal).
The equi-recursive view exposes the true semantics: unfolding \mu X.\,T
forever produces an infinite tree, but a regular one — it has only finitely
many distinct subtrees, so it is finitely representable as a cyclic graph. Deciding equality or
subtyping of such trees is exactly deciding bisimilarity of finite automata: decidable, and the reason
TypeScript can happily accept mutually recursive interfaces.
Encoding a list in code
We can simulate the iso-recursive discipline directly. The functor
F(X)=\langle\mathsf{nil},\ \mathsf{cons}:\{\mathsf{head}:\mathsf{Nat},\ \mathsf{tail}:X\}\rangle
is one layer; roll and unroll are our
\mathsf{fold} and \mathsf{unfold}. The knot is tied
by an interface that refers to itself.
// One layer of list structure, parameterised by "the rest": this is F(X).
type ListF<X> = { tag: "nil" } | { tag: "cons"; head: number; tail: X };
// The recursive type μX. F(X): tie the knot by self-reference.
interface NatList { readonly body: ListF<NatList>; }
const roll = (b: ListF<NatList>): NatList => ({ body: b }); // fold : F(μ) -> μ
const unroll = (l: NatList): ListF<NatList> => l.body; // unfold: μ -> F(μ)
const nil: NatList = roll({ tag: "nil" });
const cons = (h: number, t: NatList): NatList => roll({ tag: "cons", head: h, tail: t });
// Every use of the list UNFOLDS one layer, then recurses on the tail.
function sum(l: NatList): number {
const f = unroll(l);
return f.tag === "nil" ? 0 : f.head + sum(f.tail);
}
function length(l: NatList): number {
const f = unroll(l);
return f.tag === "nil" ? 0 : 1 + length(f.tail);
}
const xs = cons(3, cons(1, cons(4, cons(1, nil))));
console.log("list = [3, 1, 4, 1]");
console.log("length =", length(xs)); // 4
console.log("sum =", sum(xs)); // 9
A binary tree is the same trick with two recursive occurrences:
\mathsf{Tree} = \mu X.\ \langle \mathsf{leaf}:\mathsf{Nat},\ \mathsf{node}:\{\mathsf{l}:X,\ \mathsf{r}:X\}\rangle.
Every algebraic data type you have ever written is a \mu over a variant of
records — Haskell's data, Rust's enum, ML's datatype all elaborate
to exactly this.
Recursive types tame the Y combinator
In the untyped lambda calculus, recursion comes from self-application — the fixed-point
combinator Y = \lambda f.\,(\lambda x.\,f\,(x\,x))\,(\lambda x.\,f\,(x\,x))
hinges on the sub-term x\,x. The simply typed lambda calculus flatly
rejects x\,x: for x to be applied to
itself, its type would have to satisfy X = X \to T, an equation STLC's finite
types cannot solve. That is why STLC is strongly normalising — and why it cannot express
general recursion.
Recursive types solve that equation. Put
D = \mu X.\ X \to T. Now a value of type D
can be applied to a value of type D, because
\mathsf{unfold} turns it into a D \to T. With that
one type we can write a well-typed fixed-point operator:
\mathsf{fix}_T : (T \to T) \to T,
\qquad\text{using}\quad \omega = \lambda x{:}D.\ f\,\big((\mathsf{unfold}\ x)\,x\big).
The moral is stark: adding \mu to STLC makes it Turing-complete.
Self-application returns, non-termination returns, and strong normalisation is lost. Recursive types buy
expressive power at the exact price of totality — a trade every general-purpose language accepts, and
every proof assistant refuses.
Unfold \mathsf{NatList}=\mu X.\langle\mathsf{nil},\mathsf{cons}:\{\mathsf{head}:\mathsf{Nat},\mathsf{tail}:X\}\rangle
and you get an infinitely deep tree: cons-of-cons-of-cons forever. Yet the compiler stores it in a few
bytes. The secret is that the tree is regular — it has only finitely many distinct
subtrees (here, just one shape repeating), so it can be drawn as a finite graph with a back-edge, a
so-called rational tree. Deciding whether two such infinite trees are equal, or one is a subtype
of the other, becomes a question about finite automata and is perfectly decidable. Infinity, folded into
a cycle, is why your editor can autocomplete a linked list without running forever.
In domain theory one distinguishes the least fixed point (finite data — inductive lists that
must end) from the greatest (possibly infinite data — coinductive streams that need not). The
plain \mu X.\,T of a general-purpose language is neither: it is an
unrestricted fixed point that admits both finite lists and infinite/⊥-valued ones,
because — as the Y-combinator encoding shows — recursive types make every type inhabited by a
non-terminating term. Do not assume a value of a recursive type is finite or that recursion over it
terminates; the type system no longer promises it. Languages that do want the guarantee (Coq,
Agda, Idris) split \mu into separate inductive and
coinductive types and impose termination/productivity checks — precisely to buy back the
totality that unrestricted \mu throws away.