Online ISSN:1349-8606
Progress in Informatics  
No.10 March 2013  
Page 3-18 PDF(1158KB) | References
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)
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.
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.
Go back HOME