| doi:10.2201/NiiPi.2013.10.2 |
| Distributive laws of directed containers |
| Danel AHMAN1 and Tarmo UUSTALU2 |
1Laboratory for Foundations of Computer Science, University of Edinburgh
2Institute of Cybernetics, Tallinn University of Technology |
(Received: June 10,2012)
(Revised: November 6,2012)
(Accepted: December 22,2012) |
Abstract:
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 distributive-law based composition construction of directed containers. This turns out to generalize the Zappa-Szép product of two monoids.
|
Keywords:
directed containers, comonads, distributive laws, monoids, Zappa-Szép products, mathematical structures in functional programming, dependently typed programming
|
|
|
| PDF(1158KB) | References |
National Institute of Informatics is a member of CrossRef.
|
