Distributive laws of directed containers
Danel Ahman, Tarmo Uustalu · Progress in Informatics · 2013
Containers are an elegant representation of a wide class of datatypes in terms of positions and shapes.We have recently introduced directed containers as a special case to account for the common situation where every position in a shape determines another shape, informally the subshape rooted by that position.While containers interpret into set functors via a fully faithful functor, directed containers denote comonads fully faithfully.In fact, directed containers correspond to exactly those containers that carry a comonad structure.Directed containers can also be seen as a generalization (a dependently typed version) of monoids.While the category of containers (just as the category of set functors) carries a composition monoidal structure, directed containers (just as comonads) do not generally compose.In this paper, we develop a concept of a distributive law between two directed containers corresponding to that of a distributive law between two comonads and spell out the distributivelaw based composition construction of directed containers.This turns out to generalize the Zappa-Szép product of two monoids.