Container (type theory)

For lists, the shape type is the natural numbers (including zero). The corresponding position types are the types of natural numbers less than the shape, for each shape.

For trees, the shape type is the type of trees of units (that is, trees with no information in them, just structure). The corresponding position types are isomorphic to the types of valid paths from the root to particular nodes on the shape, for each shape.

Note that the natural numbers are isomorphic to lists of units. In general the shape type will always be isomorphic to the original non-generic container type family (list, tree etc.) applied to unit.

One of the main motivations for introducing the notion of containers is to support generic programming in a dependently typed setting.

Categorical aspects

The extension of a container is an endofunctor. It takes a function g to

${\displaystyle \lambda (s,f).(s,g\circ f)}$

This is equivalent to the familiar map g in the case of lists, and does something similar for other containers.

Containers form a category in which a morphism from ${\displaystyle S◃P}$ to ${\displaystyle T◃Q}$ is a function ${\displaystyle u:S\to T}$ on shapes together with functions ${\displaystyle h_s:Q(us)\to Ps}$ mapping positions backwards; it acts on extensions by ${\displaystyle \lambda (s,f).(us,f\circ h_s)}$. Extension is a full and faithful functor into endofunctors: natural transformations — in particular polymorphic functions such as reverse — correspond exactly to container morphisms, and are thereby determined by a first-order action on shapes and positions.

Containers are closed under sums, products, composition, and least and greatest fixed points. The initial algebra of the extension of ${\displaystyle S◃P}$ is the W-type (type of wellfounded trees) ${\displaystyle {\mathsf{W}}_{s:S}Ps}$ of Martin-Löf type theory, so every strictly positive type — including nested inductive types — is the extension of a container. Over the category of sets, extensions of containers coincide with the one-variable polynomial functors, and the theory can be developed in any locally cartesian closed category with W-types in the categorical sense of Moerdijk and Palmgren.

Containers also admit a formal derivative, whose shapes are shapes with one distinguished position (a "one-hole context"); it obeys laws analogous to those of differential calculus and underlies zipper structures. The containers whose extension carries a comonad structure are exactly the directed containers, such as nonempty lists, where the comonadic structure is given by taking suffixes.