In object-oriented programming, there are many notions of
‘collection with members in X’.
This paper offers an axiomatic theory of collections based on monads in
the category of sets
and total functions. Heuristically, the axioms defining a collection
monad state that each
collection has a finite set of members of X, that pure
1-element collections exist and that a
collection of collections flattens to a single collection whose members
are the union of the
members of the constituent collections. The relationship between monads
and universal
algebra leads to a formal definition of collection implementation in terms
of tree-processing.
Ideas from elementary category theory underly the classification of collections.
For example,
collections can be zipped if and only if the monad's endofunctor
preserves pullbacks. Or, a
collection can be uniquely specified by its shape and list of data if the
morphisms of the
Kleisli category of the monad are all deterministic, and the converse holds
for commutative
monads. Again, a collection monad is ordered if the
monad's functor preserves equalizers of
monomorphisms (so, in particular, if collections can be zipped the monad
is ordered). Every
implementable monad is ordered. It is shown using the well-ordering principle
that a
collection monad is ordered if and only if its functor admits an appropriated
list-valued
natural transformation that lists the members of each collection.