paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The graphical theory of monads

单子的图形理论
JFP vol.352025匹配度 2/10 · 该论文属于纯范畴论/形式语义方向,用弦图重述单子的形式理论,虽与编程语言语义基础相关,但未涉及用户核心关注的 PL→AI、AI→PL、浮点程序分析或贝叶斯程序分析,也无 LLM/Agent、静态分析或工业落地内容。引用 0 inbox
RALF HINZE, DAN MARSDEN
crossref: 2026-09-10

AI 速览

一句话:用弦图给出单子的形式理论,使 Eilenberg–Moore/Kleisli 分解、提升与分配律等可用图形化计算统一推导。

单子的形式理论表明,许多单子理论可在 2-范畴层面抽象展开,从而使相关结果一次建立并实例化到富范畴等场景。然而,这种抽象机制涉及较高阶的结构,推导与理解往往较为困难。本文用弦图——一种面向 2-范畴计算的图形语言——重新表述单子的形式理论。作者展示,Eilenberg–Moore 与 Kleisli 分辨率、提升(liftings)以及分配律等单子理论的核心内容,都可以通过系统的图形化演算来理解与推导。文章兼具双重目的:既作为单子形式理论的导论,也作为弦图及其在单子理论计算中应用的入门。

问题
单子的形式理论虽能在 2-范畴层面抽象建立,但涉及高阶抽象机制,导致推导与理解困难。
方法
使用弦图作为 2-范畴计算的图形语言,重新表述单子的形式理论,并以图形化演算推导关键构造。
评估
通过展示 Eilenberg–Moore 与 Kleisli 分辨率、提升、分配律等经典结果均可由图形推导演绎,论证该视角的计算与教学价值;本文主要作为形式单子论与弦图的导论。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@article{HinzeM25,
  title = {The graphical theory of monads},
  author = {RALF HINZE and DAN MARSDEN},
  journal = {Journal of Functional Programming},
  volume = {35},
  year = {2025},
  doi = {10.1017/s095679682500005x}
}