一句话:提出函子-函子与 monad-comonad 交互定律,统一刻画带效应计算与效应机器行为的交互,并联系有状态 runner。
论文引入函子-函子与 monad-comonad 交互定律,以描述带效应计算与执行效应机器行为之间的交互。核心结果是将 monad-comonad 交互定律刻画为函子-函子交互定律幺半范畴中的幺半对象;在对偶与 Sweedler 对偶的适当推广下,与给定函子或 comonad 交互的最大函子/monad 是其对偶,而与给定 monad 交互的最大 comonad 是其 Sweedler 对偶。作者还将这些交互定律与 stateful runner 联系起来,并证明函子-函子交互定律是内函子范畴上带 Day 卷积的 Chu 空间;Hasegawa glueing 给出的幺半结构中,其幺半对象正是 monad-comonad 交互定律。
We introduce and study functor-functor and monad-comonad interaction laws as mathematical objects to describe interaction of effectful computations with behaviors of effect-performing machines. Monad-comonad interaction laws are monoid objects of the monoidal category of functor-functor interaction laws. We show that, for suitable generalizations of the concepts of dual and Sweedler dual, the greatest functor resp. monad interacting with a given functor or comonad is its dual while the greatest comonad interacting with a given monad is its Sweedler dual. We relate monad-comonad interaction laws to stateful runners. We show that functor-functor interaction laws are Chu spaces over the category of endofunctors taken with the Day convolution monoidal structure. Hasegawa's glueing endows the category of these Chu spaces with a monoidal structure whose monoid objects are monad-comonad interaction laws.
DOI 原文 ·
@inproceedings{paperbot5522,
title = {Interaction Laws of Monads and Comonads},
author = {Shin-ya Katsumata and Exequiel Rivas and Tarmo Uustalu},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394808}
}