In
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a fou ...
, containers are abstractions which permit various "collection types", such as
lists and
trees
In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, including only woody plants with secondary growth, plants that are u ...
, to be represented in a uniform way. A (
unary) container is defined by a type of ''shapes'' S and a type family of ''positions'' P, indexed by S. The ''extension'' of a container is a family of dependent pairs consisting of a shape (of type S) and a function from positions of that shape to the element type. Containers can be seen as
canonical form
In mathematics and computer science, a canonical, normal, or standard form of a mathematical object is a standard way of presenting that object as a mathematical expression. Often, it is one which provides the simplest representation of an ...
s for collection types.
For lists, the shape type is the
natural number
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''cardinal ...
s (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
Generic programming is a style of computer programming in which algorithms are written in terms of types ''to-be-specified-later'' that are then ''instantiated'' when needed for specific types provided as parameters. This approach, pioneered b ...
in a
dependently typed setting.
Categorical aspects
The extension of a container is an
endofunctor
In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) are associated to topological spaces, and ...
. It takes a function
g to
This is equivalent to the familiar
map g in the case of lists, and does something similar for other containers.
Indexed containers
Indexed containers (also known as dependent polynomial functors) are a generalisation of containers, which can represent a wider class of types, such as vectors (sized lists).
[
]
The element type (called the ''input type'') is indexed by shape and position, so it can vary by shape and position, and the extension (called the ''output type'') is also indexed by shape.
See also
*
Container (abstract data type)
In computer science, a container is a class or a data structureEntry ''data structure'' in the Encyclopædia Britannica (2009Online entryAccessed 4 Oct 2011. whose instances are collections of other objects. In other words, they store objects i ...
*
Polynomial functor (type theory)
References
External links
Container Typesblog
Type theory
{{type-theory-stub