Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of "centre", and more generally "centrality", i.e. the property for an effect to commute with all other effects, may be formulated for strong monads acting on symmetric monoidal categories. We identify three equivalent conditions which characterise the existence of the centre of a strong monad (some of which relate it to the premonoidal centre of Power and Robinson) and we show that every strong monad on many well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. More generally, we study central submonads, which are necessarily commutative, just like the centre of a strong monad. We provide a computational interpretation by formulating equational theories of lambda calculi equipped with central submonads, we describe categorical models for these theories and prove soundness, completeness and internal language results for our semantics.
翻译:范畴论中的单子是代数结构,可用于编程语言中建模计算效应。我们展示了如何在对称幺半范畴上作用的强单子中表述“中心”(centre)以及更一般的“中心性”(centrality)概念——即某效应与所有其他效应可交换的性质。我们识别出三个等价条件,用于刻画强单子中心的存在性(其中部分条件将其与Power和Robinson的预幺半中心相关联),并证明在许多常见的自然范畴上,每个强单子都允许中心,从而表明这一新概念的普遍性。更一般地,我们研究必然可交换的中心子单子(central submonads),正如强单子的中心一样。通过为携带中心子单子的λ演算构建等式理论,我们给出其计算解释,描述这些理论的范畴模型,并证明我们语义的可靠性、完备性与内部语言结果。