The name “container” might be a bit misleading. For programmers, it refers to a data structure
that carries other elements. A tree, a list, a dictionnary, all those are “containers”, but
what we are looking at here are polynomial functors in the category of types. Concretely,
this means that they describe data structures such as lists and dictionaries. But they
aren’t lists or dictionaries themselves.
The definition of containers is deceptively simple. It’s a pair of a type and a second
type indexed by the first. Abbott \cite{abbottCategoriesContainers2003}
writes (S⊳P) for the container with shapes S:Set and positions P:S→Set, in this work, because we focus on the interactive nature of containers, we are going to call the indexing part the request and the indexed part the response.
Definition
A Container is a pair of a type of requests and a type of responses indexed by the request.
record Container where constructor (!>) request : Type response : request -> Type
We use a visually similar operator !> as a constructor and even allow it to be binding so that we can write (s : S) !> P s.
We also define a couple of smart constructors that simplify the declaration of containers.
The first one allows to define a container with a set of responses that does not depend on
the request.
(:-) : Type -> Type -> Container(:-) req res = (x : req) !> res
There are a number of container with special meanings, for now we define them
as monoidal units but we will come back to their semantics once we use them for implementing programs.
Definition
The neutral for tensor and composition.
I : ContainerI = Unit :- Unit
Definition
The neutral for products
One: ContainerOne = Unit :- Void
Definition
The neutral for coproducts.
Zero : ContainerZero = Void :- Void
`> [!definition]
The function associated with running a container
idris
public export
continuation : Container → Type
continuation c = (x : c.request) → c.response x