(Directed) Containers and Representing Parameterised Data Types

Containers of Abbott, Altenkirch, and Ghani are a representation of a wide class of (polynomial) set functors (that one can use to model parameterised data types) in terms of shapes and positions. Morphisms of containers represent polymorphic functions between these data types. I will present their basic theory.

I will also present a refinement of containers, called directed containers, which I have studied over the years jointly with James Chapman and Tarmo Uustau, and that naturally model data types in which there is a natural notion of sub-structure. These have a similarly natural category-theoretic characterisation to containers, in that they represent comonads on the underlying set functors. They also have a neat algebraic structure, in that they equip an underlying container with a suitably dependently typed monoid and monoid action structure.