一句话:用弦图给出单子的形式理论,使 Eilenberg–Moore/Kleisli 分解、提升与分配律等可用图形化计算统一推导。
单子的形式理论表明,许多单子理论可在 2-范畴层面抽象展开,从而使相关结果一次建立并实例化到富范畴等场景。然而,这种抽象机制涉及较高阶的结构,推导与理解往往较为困难。本文用弦图——一种面向 2-范畴计算的图形语言——重新表述单子的形式理论。作者展示,Eilenberg–Moore 与 Kleisli 分辨率、提升(liftings)以及分配律等单子理论的核心内容,都可以通过系统的图形化演算来理解与推导。文章兼具双重目的:既作为单子形式理论的导论,也作为弦图及其在单子理论计算中应用的入门。
Abstract The formal theory of monads shows that much of the theory of monads can be developed in the abstract at the level of 2-categories. This means that results about monads can be established once and for all and simply instantiated in settings such as enriched category theory. Unfortunately, these results can be hard to reason about as they involve more abstract machinery. In this paper, we present the formal theory of monads in terms of string diagrams — a graphical language for 2-categorical calculations. Using this perspective, we show that many aspects of the theory of monads, such as the Eilenberg–Moore and Kleisli resolutions of monads, liftings, and distributive laws, can be understood in terms of systematic graphical calculational reasoning. This paper will serve as an introduction both to the formal theory of monads and to the use of string diagrams, in particular, their application to calculations in monad theory.