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] }

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** (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.

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* : *R* → *S* 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.

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.

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 *n*th exterior power functor, and the vertical diagram with *n* cells corresponds to the *n*th 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 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. - ↑ 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)

- Container Types blog

This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it. |

This page is based on this Wikipedia article

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.