Danel Ahman: On monads and comonads for bidirected containers

Speaker: Danel Ahman

Abstract: Containers of Abbott, Altenkirch, and Ghani are a representation of a wide class of (polynomial) set functors (that one can use to model parameterised datatypes) in terms of shapes and positions. Morphisms of containers represent polymorphic functions between these datatypes.

Directed containers of Ahman, Chapman, and Uustalu characterise those containers that capture datatypes in which every position in a data-structure determines another data-structure, informally, the sub-data-structure rooted by that position, e.g., as in non-empty lists and node-labelled trees. Algebraically, this is expressed by requiring positions to have a dependently typed monoid-like structure, together with an action of this structure on the shapes.

Directed containers turn out to exactly capture those containers whose interpretation carries a comonad structure. Directed containers also enjoy a cointerpretation into (update) monads, which one can use to model effectful computations in terms of states and updates. From a different viewpoint, the category of directed containers is equivalent to the opposite of the category of small categories and cofunctors.

In this talk, I will discuss bidirected containers. These are directed containers in which it is possible to canonically undo any movements into sub-data-structures, e.g., as in zipper datatypes. Algebraically, this means working with a group-like structure instead of a monoid-like one. In terms of small categories, bidirected containers correspond to groupoids. In particular, I will identify the class of comonads that exactly correspond to bidirected containers when the underlying functors are interpretations of containers. I will also identify the class of (update) monads that one can cointerpret bidirected containers into. These are called inverse comonads and inverse monads, respectively.