Distributive laws of directed containers
Distributive laws of directed containers
复制标题
有向容器的分配律
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Tarmo Uustalu
中科院分区：
文献类型：
--
作者：
Danel Ahman;Tarmo Uustalu
容器在位置和形状方面很好地表示了一大类数据类型。我们最近引入了有向容器作为特殊情况，以解决形状中的每个位置确定另一个形状的常见情况，非正式地，确定以该位置为根的子形状。当容器通过完全忠实的函数器解释为集合函数符时，定向容器则完全忠实地表示comonad。事实上，定向容器正好对应于那些携带联合结构的容器。定向容器也可以被视为么半群的泛化(依赖类型化的版本)。虽然容器范畴(就像集合函数符范畴一样)具有合成单态结构，但有向容器(就像合成词一样)通常不合成。本文提出了两个有向容器之间的分配律的概念，并给出了基于分配律的有向容器的合成结构。这证明推广了两个么半群的Zappa-Szép积。
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.
影响因子：
1.1
作者：
Altenkirch, Thorsten;Ghani, Neil;Morris, Peter
通讯作者：
Morris, Peter