List object

In category theory, an abstract branch of mathematics, and in its applications to logic and theoretical computer science, a list object is an abstract definition of a list, that is, a finite ordered sequence.

Formal definition

Let C be a category with finite products and a terminal object 1. A list object over an object A of C is:

an object L_A,
a morphism o_A : 1 → L_A, and
a morphism s_A : A × L_A → L_A

such that for any object B of C with maps b : 1 → B and t : A × B → B, there exists a unique f : L_A → B such that the following diagram commutes:

where〈id_A, f〉denotes the arrow induced by the universal property of the product when applied to id_A (the identity on A) and f. The notation A* (à la Kleene star) is sometimes used to denote lists over A.^[1]

Equivalent definitions

In a category with a terminal object 1, binary coproducts (denoted by +), and binary products (denoted by ×), a list object over A can be defined as the initial algebra of the endofunctor that acts on objects by X ↦ 1 + (A × X) and on arrows by f ↦ [id₁,〈id_A, f〉].^[2]

Examples

In Set, the category of sets, list objects over a set A are simply finite lists with elements drawn from A. In this case, o_A picks out the empty list and s_A corresponds to appending an element to the head of the list.
In the calculus of inductive constructions or similar type theories with inductive types (or heuristically, even strongly typed functional languages such as Haskell), lists are types defined by two constructors, nil and cons, which correspond to o_A and s_A, respectively. The recursion principle for lists guarantees they have the expected universal property.

Properties

Like all constructions defined by a universal property, lists over an object are unique up to canonical isomorphism.

The object L₁ (lists over the terminal object) has the universal property of a natural number object. In any category with lists, one can define the length of a list L_A to be the unique morphism l : L_A → L₁ which makes the following diagram commute:^[3]

References

^ Johnstone 2002, A2.5.15.
^ Philip Wadler: Recursive types for free! University of Glasgow, July 1998. Draft.
^ Johnstone 2002, p. 117.

Johnstone, Peter T. (2002). Sketches of an Elephant: a Topos Theory Compendium. Oxford: Oxford University Press. ISBN 0198534256. OCLC 50164783.