Container

Defined in abbott2004-containers. Way of representing strictly positive types, and for generic programming. It provides semantics for inductive families of types.

Kinds

Unary Containers

Unary containers have signatures $\mathrm{Set}\to \mathrm{Set}$.

$$\begin{array}{r}S:Set\\ P:S\to Set\\ (S◁P)X=\sum _{s:S}{X}^{Ps}\end{array}$$

$n$-ary Containers

An $n$-ary container is made from a ${\mathrm{Set}}^n\to \mathrm{Set}$.

$$\begin{array}{r}S:Set\\ P:[n]\to S\to Set\\ (S◁P)X=\sum _{s:S}\prod _{i:[n]}{X}_i^{Pis}\end{array}$$

Indexed Containers

An indexed container is a functor of type,

$${\mathbf{Set}}^I\to {\mathbf{Set}}^J$$

Where ${\mathbf{Set}}^I$ is an $I$ indexed family of sets, AKA a comma category in $\mathbf{Set}$.

$$\begin{array}{rl}I& :Set\\ S& :I\to Set\\ P& :(i:I)\to Si\to (j:I)\to Set\\ (S◁P)X& :=\Pi i:I.\Sigma s:Si.(j:I)\to Pi(sj)\to X\end{array}$$

TODO: Check this.

Generalized Containers

Generalized containers act as functors from an arbitrary category $\mathcal{C}$ to $\mathbf{Set}$ They can be parameterized as polynomial functors into a ‘shape’ part and a ‘position’ part:

S : Set  
P : S -> Set

Containers are a special case of polynomial functors. Containers act semantically as polynomial functors: $[[S◃P]]X=\Sigma s:S.Ps\to X$ Note, it is supposed to be $◁$ , not $▷$, as some texts use. This can be seen when written in exponential notation as: $[[S◃P]]X={\sum }_{s:S}{X}^{Ps}$

Operations

Coproducts

All containers are closed under coproduct.

Let $(S◁P),(T◁Q)$ be containers. Then

$$\begin{array}{rl}((S◁P)+(T◁Q))X& =(\Sigma s:S.X^{Ps})+(\Sigma t:T.X^{Qt})\\ & =\Sigma (s,t):S\text{texttimes}T.X^{Ps}+X^{Qt}\\ & =\Sigma (s,t):S\text{texttimes}T.X^{\text{case}(Ps)(Qt)}\\ & =(S\text{texttimes}T)◁\lambda (s,t).\mathrm{case}(Ps)(Qt)\end{array}$$

Products

Unary, nary and indexed all have products In the generalised case, the category must have infinite coproducts to have $\mathcal{C}$ closed under infinite products. damato2025-container-thesis (1.5.5)

$$\begin{array}{rl}((S◁P)\text{texttimes}(T◁Q))X& =(\Sigma s:S.X^{Ps})\text{texttimes}(\Sigma t:T.X^{Qt})\\ & =\Sigma (s,t):S\text{texttimes}T.X^{Ps}\text{texttimes}{X}^{Qt}\\ & =\Sigma (s,t):S\text{texttimes}T.X^{Ps+Qt}\end{array}$$

Composition

Unary, nary and indexed all have products. It does not make sense to talk about composition of generalized containers.

$$\begin{array}{rl}((S◁P)\circ (T◁Q))X& =\Sigma s:S.(\Sigma t:T.X^{Qt}{)}^{Ps}\\ & =\Sigma s:S.(\Sigma t:T^{Ps}.X^{Qt\text{texttimes}Ps})\\ & =\Sigma s:(\Sigma s,t:S.T^{Ps}).X^{Qt\text{texttimes}Ps}\\ & =((\Sigma s,t:S.T^{Ps})◁\Sigma p:Ps.Q(tp)\end{array}$$

Exponentiation

Equally all containers are closed under exponentiation. That is, for a pair of contianers $(S◁P)$, $(T◁Q)$, the type of container homomorphisms can be represented interally as,

$$\begin{array}{rl}((T◁Q{)}^{(S◁P)})X& =\mathrm{Hom}[(S◁P)X,(T◁Q)X]\\ & =\mathrm{Hom}[\Sigma s:S.Ps\to X,\Sigma t:T.Qt\to X]\\ & =(\Sigma f:S\to T.\Pi x:S.Q(fx)\to Px)X\\ & =T^S◁P^{\Pi }x:S.Q(fx)\to Px\end{array}$$

Properties

Construction

A type may have its extension taken ($[[\_]]$), or it may instead be passed to a fixpoint operator, such as W, to get an inductive tree, or M to get a coinductive tree, in both cases, the type is equal to its extension:

$$\begin{array}{r}[[S◁P]]X=X\end{array}$$

This resulting objects has itself as its ‘payload’. $[[\_]]$ is a fully faithful functor

Container morphisms

container homomorphisms are precisely natural transformations under $[[\_]]$.

Examples

Empty Container

The empty container has no shapes.

$$\begin{array}{rlr}0◁0& & \\ W(0◁0)& \cong & 0◁0\\ M(0◁0)& \cong & 0◁0\end{array}$$

Constant Container

A constant container ignores $X$ and produces a constant shape $C$, where positions are empty for all $s$ in $C$.

$$\begin{array}{rlr}C◁0& & \\ W(C◁0)& \cong & C\\ M(C◁0)& \cong & C\end{array}$$

Identity Container

$$\begin{array}{rl}\mathrm{Identity}X& =X=(1◁1)X\\ W\mathrm{Identity}& \cong \perp \\ M\mathrm{Identity}& \cong \mathrm{Type}(?)\end{array}$$

Maybe Container

$$\begin{array}{rl}\mathrm{Maybe}X& =1+X=(2◁\{0\mapsto \perp ;1\mapsto \top \})\\ W\mathrm{Maybe}& \cong \mathbb{N}\\ M\mathrm{Maybe}& \cong \mathrm{Co}\mathbb{N}\end{array}$$

Simple Product Container

$$\begin{array}{rl}\mathrm{Product}XY& =X\text{texttimes}Y\cong (X◁\lambda \_\to \top )Y\\ W(\mathrm{Product}X)& \cong \perp \\ M(\mathrm{Product}X)& \cong \mathrm{Stream}X\end{array}$$

MaybeProd Container

$$\begin{array}{rl}\mathrm{MaybeProd}AX& =1+X\text{texttimes}Y\\ W(\mathrm{MaybeProd}X)A& \cong \mathrm{List}A\\ M(\mathrm{MaybeProd}X)A& \cong \mathrm{LazyList}A\end{array}$$

Square Container

$$\begin{array}{rl}\mathrm{Square}X& =X\text{texttimes}X\\ W\mathrm{Square}& \cong \perp \\ M\mathrm{Square}& \cong \mathrm{InfiniteBinTree}\top \end{array}$$

MaybeSquare Container

$$\begin{array}{rl}\mathrm{MaybeSquare}X& =1+X\text{texttimes}X\\ W\mathrm{MaybeSquare}& \cong \mathrm{BinTree}\top \\ M\mathrm{MaybeSquare}& \cong \mathrm{LazyBinTree}\top \end{array}$$

List Container

$$\begin{array}{rl}\mathrm{List}X& =\mathbb{N}◁\mathrm{Fin}\\ W\mathrm{List}& \cong \mathrm{RoseTree}\top \\ M\mathrm{List}& \cong \mathrm{LazyRoseTree}\top \end{array}$$

CoList Container

$$\begin{array}{rl}\mathrm{CoList}X& =\mathrm{Co}\mathbb{N}◁\mathrm{CoFin}\\ W\mathrm{CoList}& \cong \mathrm{CoBranchingRoseTree}\top \\ M\mathrm{CoList}& \cong \mathrm{CoRoseTree}\top \end{array}$$

Stream Container

$$\begin{array}{rl}\mathrm{List}X& =\top ◁\mathbb{N}\\ W\mathrm{List}& \cong \perp \\ M\mathrm{List}& \cong \text{Set of integer sequences}\top \end{array}$$

Category theoretic perspective

Containers are presented as constructions in the internal language of Locally Cartesian Closed Category Initial Algebra is W Types Terminal coalgebra of a container is an M type.

Remarks

fiore2022-quotient-inductive refers to this as a signature. It is unclear where that terminology arises form.

References

damato2025-formalizing-containers Chapter 1 - overall survey. abbott2004-containers

# Duplicate Content 1

Defined in [[abbott2004-containers]]. Way of representing [[strictly positive types]].

S : Set P : S → Set

Containers act semantically as polynomial functors:
$(S\triangleleft P) X = \Sigma s:S. P s \to X$ 
[[Initial algebra]] is [[W Type|W Types]]
Container 
[[Terminal coalgebra]] of a container is an [[M type]]. 
Coniductive principle: if you have a bisimulation on streams

## References 
 [[damato2025-formalizing-containers]]
 [[abbott2004-containers]]