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 of C is:
such that for any object of with maps : 1 → and : × →, there exists a unique : → such that the following diagram commutes:
[Image:List object definition.svg|300px|A commutative diagram expressing the equations in the definition of a list object]
where〈id, 〉denotes the arrow induced by the universal property of the product when applied to id and. The notation * is sometimes used to denote lists over.
Equivalent definitions
In a category with a terminal object 1, binary coproducts, and binary products, a list object over can be defined as the initial algebra of the endofunctor that acts on objects by ↦ 1 + and on arrows by ↦ .Examples
- In Set, the category of sets, list objects over a set are simply finite lists with elements drawn from. In this case, picks out the empty list and corresponds to appending an element to the head of the list.
- In the calculus of inductive constructions or similar type theories with inductive types, lists are types defined by two constructors, nil and cons, which correspond to and , 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 1 has the universal property of a natural number object. In any category with lists, one can define the length of a list to be the unique morphism : → 1 which makes the following diagram commute:
[Image:List object length.svg|350px|A commutative diagram expressing the equations in the definition of the length of a list object]