Encoding arbitrary algebraic data types in set theory?

Question

Natural numbers are often defined recursively as an algebraic data type:

type Nat :=
 | Zero
 | Succ of Nat

In set theory/ZFC, we can define the natural numbers without depending on recursive definitions:

def $0:= ∅$
def $\text{Succ}(n) := n ∪ \{n\} $
def $\text{isNatLike}(n) := (n = 0) ∨ (∃x, n = \text{Succ}(x))$

def $\mathbb{N} := \{n\;|\;\text{isNatLike}(n) ∧ ∀x ∈ n, \text{isNatLike}(x)\}$

It can be shown that Peano axioms follow from this definition under ZFC.

The definition is nontrivial, but it allows us to construct the algebraic data type in first order logic, using a framework which does not inherently support recursive definitions.

Given an arbitrary algebraic data type, is it always possible to encode the type in ZFC? Is there an algorithm for performing this construction?

Answer 1

Algebraic data types are usually explained in terms of initial algebra semantics. The way that this works is that you have a category $\cal S$ that allows types/contexts to be interpreted as objects and terms as arrows. Then, a data type definition has an associated functor $F : \cal S → \cal S$ encoding its 'shape'. For $ℕ$ this is $1 + -$. In general, the functor for a data type definition is built by:

1. recursive occurrences correspond to the identity functor
2. other type formations work point-wise
3. multiple arguments of a constructor are combined as a product
4. multiple constructors are combined as a coproduct

Once we have such a functor, we consider the category of its algebras ${\cal S}_F$, which has objects:

1. an object $A$ of $\cal S$
2. an algebra action $α : F A → A$

and arrows $(A,α) → (B,β)$ are $h : A → B$ such that $h \circ α = β \circ Fh$.

If ${\cal S}_F$ has an initial object $(μF, \mathsf{in})$, then the object $μF$ is the interpretataion of the data type, $\mathsf{in} : FμF → μF$ gives the interpretations of the constructor terms, and the universal homomorphism $!_A : μF → A$ interprets the induction/recursion principle of the data type.

If $\cal S$ is the category of sets, these initial algebras generally exist when $F$ is a polynomial. This corresponds (roughly) to the syntactic criterion of a data type being "strictly positive," which means that a recursive occurrence never happens to the left of an arrow in the sum-of-products specification. The functor:

$$F X = 1 + X + (ℕ → X)$$

is strictly positive, but:

$$F X = (X → \mathbf 2) → \mathbf 2$$

is not. Some type theories have data types given by the latter functor, but classical set theoretic semantics do not support it. The syntactic definition is technically more restrictive, though; what matters is if the functor is semantically equivalent to one that can be described strictly positively.

A shorter way of describing what's going on above is that algebraic data types are a general form of inductive definition. Classical set theory can demonstrate the existence of inductively defined sets for polynomial functors, and that corresponds to a general sort of data type that can be interpreted set theoretically.