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:

  1. an object LA,
  2. a morphism oA : 1 → LA, and
  3. 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:

A commutative diagram expressing the equations in the definition of a list object

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

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
  • 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

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]

A commutative diagram expressing the equations in the definition of the length of a list object

References
  1. Johnstone 2002, A2.5.15.
  2. Philip Wadler: Recursive types for free! University of Glasgow, July 1998. Draft.
  3. Johnstone 2002, p. 117.
  • Johnstone, Peter T. (2002). Sketches of an Elephant: a Topos Theory Compendium. Oxford: Oxford University Press. ISBN 0198534256. OCLC 50164783.

See also
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.