Container (type theory)

Last updated

In type theory, containers are abstractions which permit various "collection types", such as lists and trees, 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 forms for collection types. [1]


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. [1]

Categorical aspects

The extension of a container is an endofunctor. 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). [2]

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

Related Research Articles

Ring homomorphism mapping between two rings which respects the structure

In ring theory, a branch of abstract algebra, a ring homomorphism is a structure-preserving function between two rings. More explicitly, if R and S are rings, then a ring homomorphism is a function f : RS such that f is

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 by the ML programming language in 1973, permits writing common functions or types that differ only in the set of types on which they operate when used, thus reducing duplication. Such software entities are known as generics in Python, Ada, C#, Delphi, Eiffel, F#, Java, Nim, Rust, Swift, TypeScript and Visual Basic .NET. They are known as parametric polymorphism in ML, Scala, Julia, and Haskell ; templates in C++ and D; and parameterized types in the influential 1994 book Design Patterns.

In combinatorial mathematics, the theory of combinatorial species is an abstract, systematic method for analysing discrete structures in terms of generating functions. Examples of discrete structures are (finite) graphs, permutations, trees, and so on; each of these has an associated generating function which counts how many structures there are of a certain size. One goal of species theory is to be able to analyse complicated structures by describing them in terms of transformations and combinations of simpler structures. These operations correspond to equivalent manipulations of generating functions, so producing such functions for complicated structures is much easier than with other methods. The theory was introduced, carefully elaborated and applied by the Canadian group of people around André Joyal.

Quotient ring

In ring theory, a branch of abstract algebra, a quotient ring, also known as factor ring, difference ring or residue class ring, is a construction quite similar to the quotient groups of group theory and the quotient spaces of linear algebra. It is a specific example of a quotient, as viewed from the general setting of universal algebra. One starts with a ring R and a two-sided ideal I in R, and constructs a new ring, the quotient ring R / I, whose elements are the cosets of I in R subject to special + and operations.

In combinatorics, a branch of mathematics, a matroid is a structure that abstracts and generalizes the notion of linear independence in vector spaces. There are many equivalent ways to define a matroid axiomatically, the most significant being in terms of: independent sets; bases or circuits; rank functions; closure operators; and closed sets or flats. In the language of partially ordered sets, a finite matroid is equivalent to a geometric lattice.

Intuitionistic type theory is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.

In mathematics, a scheme is a mathematical structure that enlarges the notion of algebraic variety in several ways, such as taking account of multiplicities and allowing "varieties" defined over any commutative ring.

In mathematics, an algebraic torus is a type of commutative affine algebraic group. These groups were named by analogy with the theory of tori in Lie group theory.

Group scheme group object in the category of schemes

In mathematics, a group scheme is a type of algebro-geometric object equipped with a composition law. Group schemes arise naturally as symmetries of schemes, and they generalize algebraic groups, in the sense that all algebraic groups have group scheme structure, but group schemes are not necessarily connected, smooth, or defined over a field. This extra generality allows one to study richer infinitesimal structures, and this can help one to understand and answer questions of arithmetic significance. The category of group schemes is somewhat better behaved than that of group varieties, since all homomorphisms have kernels, and there is a well-behaved deformation theory. Group schemes that are not algebraic groups play a significant role in arithmetic geometry and algebraic topology, since they come up in contexts of Galois representations and moduli problems. The initial development of the theory of group schemes was due to Alexander Grothendieck, Michel Raynaud and Michel Demazure in the early 1960s.

In mathematics, particularly category theory, a representable functor is a certain functor from an arbitrary category into the category of sets. Such functors give representations of an abstract category in terms of known structures allowing one to utilize, as much as possible, knowledge about the category of sets in other settings.

Many letters of the Latin alphabet, both capital and small, are used in mathematics, science, and engineering to denote by convention specific or abstracted constants, variables of a certain type, units, multipliers, or physical entities. Certain letters, when combined with special formatting, take on special meaning.

In mathematics, a variable is a symbol used to represent an arbitrary element of a set. In addition to numbers, variables are commonly used to represent vectors, matrices and functions.

In category theory, the concept of catamorphism denotes the unique homomorphism from an initial algebra into some other algebra.

In many programming languages, map is the name of a higher-order function that applies a given function to each element of a functor, e.g. a list, returning a list of results in the same order. It is often called apply-to-all when considered in functional form.

In mathematics, especially in the field of representation theory, Schur functors are certain functors from the category of modules over a fixed commutative ring to itself. They generalize the constructions of exterior powers and symmetric powers of a vector space. Schur functors are indexed by Young diagrams in such a way that the horizontal diagram with n cells corresponds to the nth exterior power functor, and the vertical diagram with n cells corresponds to the nth symmetric power functor. If a vector space V is a representation of a group G, then also has a natural action of G for any Schur functor .

In mathematics, KK-theory is a common generalization both of K-homology and K-theory as an additive bivariant functor on separable C*-algebras. This notion was introduced by the Russian mathematician Gennadi Kasparov in 1980.

In type theory, a system has inductive types if it has facilities for creating a new type along with constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.

In mathematics, a family, or indexed family, is informally a collection of objects, each associated with an index from some index set. For example, a family of real numbers, indexed by the set of integers is a collection of real numbers, where a given function selects for each integer one real number.

Conor McBride is a lecturer in the department of Computer and Information Sciences at the University of Strathclyde. In 1999, he completed a Doctor of Philosophy (Ph.D.) in Dependently Typed Functional Programs and their Proofs at the University of Edinburgh for his work in type theory. He formerly worked at Durham University and briefly at Royal Holloway, University of London before joining the academic staff at the University of Strathclyde.

In type theory, a polynomial functor is a kind of endofunctor of a category of types that is intimately related to the concept of inductive and coinductive types. Specifically, all W-types are initial algebras of such functors.


  1. 1 2 Michael Abbott; Thorsten Altenkirch; Neil Ghani (2005). "Containers: Constructing strictly positive types". Theoretical Computer Science. 342 (1): 3–27. doi:10.1016/j.tcs.2005.06.002.
  2. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. "Indexed Containers" (PDF). Unpublished manuscript. Retrieved 2008-10-30.Cite journal requires |journal= (help)CS1 maint: multiple names: authors list (link)