新博文用弦图讲解类型系统,图解 Monad 即自函子范畴上的幺半群
roboguy20 · x · 2026-10-18
roboguy20 发布博客《String diagrams and the monad laws》,介绍弦图(string diagrams)这一图形语言,用于讨论各类类型系统。
- 弦图假设极少:把复制(contraction)、丢弃(weakening)、交换(exchange)三条结构规则都显式画出,天然适合讨论线性类型语言。
- 图中左侧为输入、右侧为输出,对应表达式;开放表达式的输入对应自由变量,文中用 x:Nat,y:Nat ⊢ x+y:Nat 等例子说明如何把类型化表达式画成图。
- 核心成果:用弦图展示 Monad 定律如何对应幺半群定律——配图并列对比列表幺半群的结合律 (x++y)++z = x++(y++z) 与 Monad 的 join . join = join . fmap join,直观呈现「Monad 就是自函子范畴上的幺半群」。