my-server
← Wiki

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:

  1. an object <sub></sub>,
  2. a morphism <sub></sub> : 1 → <sub></sub>, and
  3. a morphism <sub></sub> : × <sub></sub> → <sub></sub>

such that for any object of with maps : 1 → and : × → , there exists a unique : <sub></sub> → such that the following diagram commutes:

<div style="margin-left: 2em"></div>

where〈id<sub></sub>, 〉denotes the arrow induced by the universal property of the product when applied to id<sub></sub> (the identity on ) and . The notation * ( Kleene star) is sometimes used to denote lists over .

Equivalent definitions

In a category with a terminal object 1, binary coproducts (denoted by +), and binary products (denoted by ×), a list object over can be defined as the initial algebra of the endofunctor that acts on objects by ↦ 1 + ( × ) and on arrows by ↦ [id<sub>1</sub>,〈id<sub></sub>, 〉].

Examples

  • In Set, the category of sets, list objects over a set are simply finite lists with elements drawn from . In this case, <sub></sub> picks out the empty list and <sub></sub> 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 <sub></sub> and <sub></sub>, 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 <sub>1</sub> (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 <sub></sub> to be the unique morphism : <sub></sub> → <sub>1</sub> which makes the following diagram commute:

<div style="margin-left: 2em"></div>

References

See also