This article needs additional citations for verification. (December 2017) |
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 edit
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 LA,
- a morphism oA : 1 → LA, and
- a morphism sA : A × LA → LA
such that for any object B of C with maps b : 1 → B and t : A × B → B, there exists a unique f : LA → B such that the following diagram commutes:
where〈idA, f〉denotes the arrow induced by the universal property of the product when applied to idA (the identity on A) and f. The notation A* (à la Kleene star) is sometimes used to denote lists over A.[1]
Equivalent definitions edit
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 ↦ [id1,〈idA, f〉].[2]
Examples edit
- In Set, the category of sets, list objects over a set A are simply finite lists with elements drawn from A. In this case, oA picks out the empty list and sA 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 oA and sA, respectively. The recursion principle for lists guarantees they have the expected universal property.
Properties edit
Like all constructions defined by a universal property, lists over an object are unique up to canonical isomorphism.
The object L1 (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 LA to be the unique morphism l : LA → L1 which makes the following diagram commute:[3]
References edit
- ^ 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.