We develop the theory of strong and commutative monads in the 2-dimensional setting of bicategories. This provides a framework for the analysis of effects in many recent models which form bicategories and not categories, such as those based on profunctors, spans, or strategies over games. We then show how the 2-dimensional setting provides new insights into the semantics of concurrent functional programs. We introduce concurrent pseudomonads, which capture the fundamental weak interchange law connecting parallel composition and sequential composition. This notion brings to light an intermediate level, strictly between strength and commutativity, which is invisible in traditional categorical models. We illustrate the concept with the continuation pseudomonad in concurrent game semantics. In developing this theory, we take care to understand the coherence laws governing the structural 2-cells. We give many examples and prove a number of practical and foundational results.
翻译:我们在双范畴的二维结构中发展了强单子与交换单子的理论。这为分析诸多基于双范畴而非范畴的现代模型中的效应提供了框架,例如基于余函子、跨度或博弈策略的模型。随后我们展示二维结构如何为并发函数式程序的语义提供新见解。我们引入并发伪单子,它刻画了连接并行组合与序列组合的基本弱交换律。这一概念揭示了一个介于强度与交换性之间的中间层——这在传统范畴论模型中是不可见的。我们通过并发博弈语义中的续延伪单子来阐明该概念。在构建该理论的过程中,我们特别关注支配结构2-胞腔的相干律。我们给出大量实例,并证明了若干实用性与基础性结果。