范畴论与 Haskell 程序设计（零）：大纲

This process of hierarchical decomposition and recomposition is not imposed on us by computers. It reflects the limitations of the human mind.
— Bartosz Milewski, Category Theory for Programmers: The Preface

序

工程学的核心是管理复杂性。面对庞大、混沌、错综交织的现实需求，我们几乎只有一种武器：分解。我们将大问题分解为小问题，将复杂的模块分解为简单的单元，这是我们作为工程师的本能，也是我们唯一的本领。这并非计算机强加于我们的思维范式，它根植于人类心智的局限性。

对于如何分解，如何抽象，如何组合，也许每一位程序员都有自己的想法。世界上有这样一群人，我们混迹各种编程话题，难免会注意到他们的存在：

• 出没在各种函数式编程社区，通篇充斥着抽象废话 (abstract nonsense)；
• 热衷于展示一些难懂的交换图，但看起来只是装模做样；
• 喜欢嘲讽任何非纯的程序语言，尤其是取笑这些语言的锁机制；
• 标榜自己的代码只在主逻辑传入参数，定义函数根本不需要形参；
• 转身打开编辑器偷偷写一些 do ... return ... 这样看上去和其他语言别无二致的东西；
• 被吃瓜群众问到以后，涨红脸说些“非纯……Monad 的事，能叫非纯吗……”这样难懂的话；
• 被要求解释一下什么是 Monad，叽里咕噜半天，什么打开盒子装进盒子，一些具体的抽象废话；
• 现实中，据说这些人真的参与大型软件项目，但谁也没在身边见过，打听来打听去，好像这些人只能混迹在银行和铁路这些老古董行业，什么？编译器？那也是老古董！

我本人并非 Haskell 程序员，甚至也不是函数式编程的拥趸。在很长一段时间里，我对“他们”的态度是，保持好奇，同时敬而远之。我不相信范畴论可以指导任何现实中的软件设计问题，我认为设计模式——连同其他面向对象设计原则——已经足够解决我在实际编码工作中遇到的所有问题了。如果说在范围之外还有别的问题，那一定涉及到如何安排开发周期，如何组织团队协作，如何面对需求变更，诸如此类，而这是软件工程的领域，和编程语言无关。

起初，我认为他们——我是指 Haskell 程序员——并没有严肃对待软件设计问题。在我看来，他们更像一群沉迷于智力游戏的数学爱好者，而非愿意弄脏双手的工程师。当我们在现实的泥潭中与并发、状态管理和异常搏斗时，他们冷漠地打量着我们，偶尔推销一些不着边际的银弹，用以解决一些仅存在于他们想象中的问题。

后来我遇到了一些困难，超出了我的认识范围，我误打误撞在 Haskell 社区中找到了需要的东西，它如此简洁、紧凑、纯粹、浑然天成，任何人看到它都会认为“没错，编程本来就是这样！”。我并不准备将这个故事放在开头，我们会在后面的章节逐渐分享它。总之，在那之后，我突然明白，对于软件设计，他们和我们的身份一样，也是勤勉而热烈的工程师，我们都勇敢且真诚地面对软件内生的复杂性^[1]。他们使用的语言和概念不是抽象废话，那是他们的哲学，他们的世界观，是一套切实可行，甚至可以说高效的工程范式，只是——只是与我们这一套不同，非常，非常不同。

然而，通往新世界的大门似乎并不情愿为外来者敞开。Haskell 社区常常给我一种极端排外的印象。他们的文字间充满各种隐晦、难以理解的暗号和密语。所谓入门材料，也大多晦涩难懂，往往在展示了 map 和 filter 的简单用法后，立即将读者抛入自函子范畴的风暴中，吝于提及沿途的风景和危险。这道——我认为是人为构筑的——鸿沟吓退了无数像我一样满怀好奇的冒险者，也让 Haskell 社区与我们距离越来越远，愈发陌生。

这份讲义是我们为后来者绘制的地图。我希望它能从我们熟悉的、经验驱动的工程世界出发，径直联接到与那个看似遥远的、由范畴论构建的形式化领域。我们绝不会回避那些艰深的概念，但我们会从直觉出发，用我们共通的工程师视角认识它们的轮廓，揭示它们在代码中的具体形态，探索它们如何解决现实的工程问题——我们终究还是乐于弄脏双手，因为我们认同自己是勤奋勇敢的工程师。

对读者的期待

严格讲，在大灾变^[2]之后的今天，学习任何领域的内容都不再需要传统意义上的“预备知识”。只要读者擅长思考和提问，有一套内化的元学习框架，那么读者必定可以从一份基础材料出发，通过向 LLM 提问从而完整掌握材料涵盖的知识。

我们期待读者对一切充满好奇，至少此刻对范畴论和函数式编程充满好奇，这是整个旅途中持续驱动读者向更远方、更深处探索的力量源泉，也是我们唯一的“硬性要求”。那些真正走完全程，在终点开启宝箱的人，并不是因为他们多么强大、多么聪明——甚至不是因为他们比别人更自律——而是因为他们有不得不奋力向前的理由，他们好奇远方的地平线之下会是怎样的风景，他们好奇宝箱里藏着什么，他们好奇站在终点回望来时路的心情，直到最后，他们在终点远眺新的地平线，整理行囊，向仍旧陌生的远方继续进发。我们心照不宣，其实马里奥从来不在乎碧姬公主^[3]，星之卡比也根本无意营救瓦豆鲁迪，不过是顺手为之，这些远非支撑冒险的理由。一切都出于——也仅仅出于——我们最原始、最强烈的情感，那便是好奇心。

不过，有些读者更习惯从书本中进入一个新领域，先建立一套连贯的概念地图，再按需查漏补缺，这是非常高效的学习习惯——即使在大灾变后也是一样。为此，我们推荐两本入门读物：

1. 《计算机程序的构造与解释》：大名鼎鼎的 SICP，如果将函数式编程看作一门真正的外语^[4]，比如英语，那 SICP 就相当于《新概念英语》。你后来意识到它有这样那样的局限和缺憾，但当你回忆对这门外语最初的感觉，那些模糊的轮廓和形貌，无一例外都源于它。你不会后悔读过它，因为是它教会你如何用这门外语思考和表达。切换到技术性的视角：在前两章，书中将 map 应用在多种数据结构上，引导读者思考背后的共性，暗示了函子 (functor) 的存在；类似还有 accumulate 暗示了幺半群对象 (monoid object)——只是 SICP 并未明文点出这些概念。同时，第二章的许多概念为 Haskell 提供了雏形，例如2.2 层次性数据和闭包性质，这一节与代数数据类型 (ADT) 有着直接关联；还有2.5 带有通用性操作的系统，我们熟悉的类型类（type class）正是在这个想法启发下诞生的。在第三章，读者会直面现实的混沌，认识纯函数和非纯函数，并养成自己的品味——你愿意为了一方面的优势而容忍另一方面的代价吗？作为整本书最深刻的“巧合”，在3.5 流这一节中，SICP 事实上在流计算中完整构造了一个 Monad——我们的讲义将会解释为何会出现这种巧合。当然，SICP 还包含无数我们没有精力提及的概念，例如惰性求值、抽象屏障等等，它们同样重要，我们鼓励读者花点时间弄明白这些概念。最后——我是说真正的最后，在读者，还有我，完成这份讲义后，演出谢幕之时——我们可以回去看看2.1.3 数据意味着什么，在范畴论的“高观点”下，我们能回答这个问题吗？
2. 《Haskell 趣学指南》：这本书可以帮助读者了解 Haskell 的基本语法，强化函数是一等公民的概念，通过 map 和 fold 巩固函数式编程的初步直觉，通过二叉树的例子接触持久化数据结构——这是纯函数式语言最地道 (idiomatic) 的数据结构。读者会接受充分的训练，学会识别 Haskell 对象的类型签名，然后越来越熟练，越来越快。我们特别推荐第十二章的走钢索，这是 Monad 最好的入门实例，如果读者在任何时候觉得自己迷失在 Monad 的森林里，都可以折回来再看一眼这个例子。况且，扮演一个走钢索的杂技演员本身也很有趣。

我们期待读者接受过基本的数学训练——别担心，请放松，继续读下去——这大致等同于说读者不患有公式恐惧症，并且赞同适当的形式化有助于更准确地、更紧凑地组织概念。人的认知资源^[5]高度有限，更紧凑的表示 (representation) 使得我们可以更自如地思考和表达。

我们期待读者在旅途中保持审慎、保持质疑。作者不是首都派驻 12 区的导师斯诺，作者和读者一样，共同参与一场盛大的冒险——只是作者出发稍早。我们同样机敏、勇敢、雄心勃勃，我们一同翻越高山，遁入深谷，但务必小心，我们也许会在峭壁上一脚踩空，在阴影中摸黑摔倒，我们在任何一处都可能犯错！也许作者将一张错误的地图交到读者手中，包括定义、概念解释、实例、隐喻、引申，乃至思维方式——这一切都有可能出错！我们鼓励读者质疑讲义中任何含糊、模棱两可、甚至看上去明显有问题的地方，鼓励读者时刻保持警惕，在作者企图蒙混过关的时候，抓住他！

最后，我们期待与读者保持沟通，评论、邮件、微信、Github issue——我们欢迎任何途径！范畴论是关于联接的科学，我们以文本为媒介与读者建立联接，我们将会看到，正是联接，让孤立的对象成为范畴，让人类个体成为人类社会，让你和我，成为我们。

符号与样式

数学部分

首先约定一下数学概念的符号和样式：

1. 范畴 (category) 使用英文草书体大写字母 \mathcal，例如一般的范畴 $\mathcal{C},\ \mathcal{D}$，还有 Hask 范畴 $\mathcal{H}$
2. 对象 (object) 使用英文意大利体大写字母，即数学环境的默认字体，例如 $A,\ B,\ X$
3. 态射 (morphism) 使用英文意大利体小写字母，例如 $f,\ g$；特别地，用 $1_{X}$ 表示对象 $X$ 的单位态射；态射复合记为 $g \circ f$；用 $\mathrm{Hom}_{\mathcal{C}}(A,\ B)$ 表示“范畴 $\mathcal{C}$ 上从对象 $A$ 到对象 $B$ 的所有态射组成的集合” ，上下文清楚时——几乎是所有时候——我们省略下标，直接记为 $\mathrm{Hom}(-,\ -)$
4. 函子 (functor) 同样使用小写字母，但使用德文尖角体 \mathfrak，以便与态射区分，例如 $\mathfrak{f},\ \mathfrak{g}$；用 $\mathfrak{f}(A)$ 和 $\mathfrak{f}(h)$ 分别表示函子 $\mathfrak{f}$ 的对象映射和态射映射
5. 自然变换 (natural transformation) 使用小写希腊字母，例如 $\alpha,\ \eta$；如要强调该变换在某对象 $X$ 上的分量 (component)，用对象名作为下标，即 $\alpha_{X}$
6. 在自函子范畴 (endofunctor category) 上，沿用德文尖角体表示自函子；特别地，恒等函子记为 $\mathfrak{id}$，函子 $\mathfrak{f}$ 到自身的恒等自然变换记为 $\mathrm{id}_{\mathfrak{f}}$；用 $\beta \circ \alpha$ 表示两自然变换的竖直复合，这与态射复合的记号保持一致；用 $\gamma * \eta$ 表示两自然变换的水平复合；此外，用 $\mathrm{Endo}(\mathcal{H})$ 表示 Hask 范畴的自函子范畴；在提及恒等函子对某对象 $X$ 的作用时，我们习惯直接用 $X$ 代替 $\mathfrak{id}(X)$
7. 积 (product) 的泛性质 (general property) 用三元组 $\{A \times B,\ p_{1},\ p_{2}\}$ 表示；另一方面，余积 (coproduct) 的泛性质用三元组 $\{A+B,\ i_{1},\ i_{2}\}$ 表示；用 $h=\left<f,\ g\right>$ 表示积和余积的态射运算
8. 用德文尖角体大写字母表示图示 (diagram)，多数时候我们不会直接给图示命名，而是直接说“以下几张图交换”；如果我们需要特别提及——譬如在定义极限和余极限时——某张图示，记为 $\mathfrak{F},\ \mathfrak{G}$

Haskell 部分

在 Haskell 语言中存在大量与范畴论对应的概念，然而，Haskell 代码没有自然语言文档这样丰富的样式，因此有必要约定清楚这些对应关系，尽量避免符号误用和混淆：

1. 原则：所有文档中的 Haskell 概念都使用等宽字体 \texttt 或 \mathtt
2. 特例：对于Hask 范畴和Hask 范畴上的自函子范畴这两个特殊概念，Haskell 语言的代码中不会显式提及它们，因此我们仍然沿用数学概念的记号 $\mathcal{H}$ 和 $\mathrm{Endo}(\mathcal{H})$
3. 范畴论中的对象，对应 Haskell 中的类型 (type)，用 $\mathtt{a,\ b,\ c,\ a1,\ a2}$ 等表示任意类型，即 Hask 范畴 $\mathcal{H}$ 中的任意对象；极少数时候，我们会提及具体的类型，例如 $\mathtt{Bool,\ Int}$ 等
4. 态射对应 Haskell 中的函数 (function)，用 $\mathtt{f,\ g}$ 等作为函数名，指代某个具体的态射，而函数类型签名体现了这个态射的源对象 (domain) 和目标对象 (codomain)，例如：
   $$\mathtt{f\ ::\ a\ \to\ b}$$
   这个函数签名表示“名为 f 的函数接受类型为 a 的输入同时输出类型为 b ”，对应到范畴论的概念上，即“态射 $f$ 将源对象 $A$ 指向目标对象 $B$ ”
5. 函子对应 Haskell 中的类型构造器 (type constructor)，例如 Maybe 和 []；必须特别注意，我们也会用 $\mathtt{f,\ g}$ 表示任意函子，我们尽力避免函子与态射的记号相互混淆，但我们无奈地承认这种可能性，读者必须根据上下文自行甄别——尤其是出现对象映射时，读者必须提高警惕；函子的态射映射 $\mathfrak{f}(h)$ 在 Haskell 中对应 fmap h :: f a -> f b，其中态射 $h$ 的类型签名为 h :: a -> b
6. 自然变换在 Haskell 上非常有趣，我们通过一个参数多态 (polymorphism) 的 Haskell 函数——这里随意命名为 eta ——来表示函子 f 到函子 g 的自然变换：
   $$\mathtt{eta\ ::\ forall\ a.\ f\ a\ \to\ g\ a}$$
   用范畴论的视角看，参数多态的 Haskell 函数其实并非一个单独的态射，而是以任意对象 $\mathtt{a}$ 为参数的一族态射 $\eta$，取参数 $\mathtt{a} = A$，得到其在对象 $A$ 上的分量为 $\eta_{A}$ ——这恰好是自然变换的定义！
7. 积在 Hask 范畴上对应元组 (tuple) (,) ，即 $\{\mathtt{(a,\ b),\ fst,\ snd}\}$，对应的态射运算为 f &&& g；而余积则对应 Either ，即 $\{\mathtt{Either\ a\ b,\ Left,\ Right}\}$，对应的态射运算为 f ||| g 或 either f g

体例

这份讲义的目标是建立以下三者的联系：

1. 范畴论
2. Haskell 编程语言
3. 现实中可以被抽象出来的典型计算过程和数据关联

瞄准目标，我们将以结构化的方式引入每一个范畴论概念。首先从直观的实例和隐喻开始，为读者建立必要的直觉。随后尝试严格化，分别使用两种视角定义并认识这个概念，即数学家的视角和 Haskell 程序员的视角。接着我们会加入更系统、更完整的 Haskell 代码实例，帮助读者进一步实现概念接地。最后，每个概念会附上 5-10 道习题。

强调数学家视角和程序员视角的差异与联系，这是本讲义贯彻始终的母题。我们坚持向读者传递这种思维方式，即对于范畴论的同一概念。数学家和程序员分别选择了“更趁手”的界面或接口（interface）。简而言之，两套接口内核一致，只是表象不同。我们将会看到，得益于 Haskell 优雅的设计，两套接口在基本概念上几乎完全一致，但对于一些进阶概念，二者之间确实存在差异，这里举一例：

对于保持了源范畴之幺半结构的函子，范畴论——即数学家的接口——使用“弱幺半函子”这个名字，而 Haskell 语言——即程序员的接口——使用 Applicative 类型类。弱幺半函子要求我们提供一个单位态射 $\phi_0$ 和一个自然变换 $\phi_1$，用于说明函子如何保持原范畴的幺半结构；而 Applicative 要求我们实现 pure 和 <*> 两个函数。乍看上去，二者是如此不同，但我们会证明两套接口可以互相实现，因此它们是等价的。

关于“如何对待数学证明”，本讲义采取的态度是：如非特别强调，默认只在 Hask 范畴 $\mathcal{H}$ 下证明定理，且只证明那些对行文逻辑必不可少的定理，毕竟这不是一本范畴论教材——那将严重偏离我们的写作动机和目标。如果可能，我们首先考虑以 Haskell 代码的形式组织证明——尤其是证明各种同构，在 Haskell 代码中，这等价于要求我们实现两个方向的函数。

内容安排

下面列出的大纲非常粗糙，为了抓住灵感，有些地方甚至不成句子，请读者见谅。后续更新的内容将按大纲分节展开。

范畴、对象与态射

范畴的定义，对象与态射的定义，Hask 范畴下的类型与函数。作为开篇，要提醒读者注意到范畴论的“世界观”，即不再关注对象的“内部结构”，转而研究“外部相互作用”，即将注意力放在态射上。放在 Hask 范畴中，这即是要求读者暂时忽略类型的值——当然同时也忽略函数的具体实现——专注于函数的类型签名。

后面我们会构造一个例子，从最简单的 $\mathtt{Bool}$ 类型入手，向读者展示从“内部视角”迁移到“外部视角”并不会丢失任何信息，不会损失语言的表达能力，其核心想法是，我们可以把类型 T 的“值” v ，v :: T，看成是某种特殊记号（语法糖），等价于从单位对象出发的态射，v :: () -> T，而内部视角下的“值” v 可以看作这个态射的唯一签名。

函子：范畴间的变换

函子的定义，Haskell 中的类型构造器。Maybe，[]，并介绍一个特殊的例子 (->) s，即固定入参类型的函数作为函子，也叫指数函子。若非特别强调，“函子”其实是“协变函子”的简称，对应某种生产容器，其态射映射对应后处理。

逆变函子（选读）

逆变（contravariant）函子（选读，首次可跳过），对比 (->) s 与 Op s，前者是协变函子，等价于 (s -> *)，后者是逆变函子，等价于 (* -> s)；逆变函子的运算 contramap :: (b -> a) -> f a -> f b，也记为 g >$< (f x)；逆变函子对应某种消费容器，其逆变态射映射对应预处理。

自然变换：函子间的变换

函子的自然变换，本节开始带领读者识别并分析交换图。我们会提供一对漂亮的实例，用 safeHead :: [a] -> Maybe a 构造一个 [] 到 Maybe 的自然变换，而反向并不构成自然变换，因此两个函子不是自然同构。本节还会介绍两个自然变换的竖直复合与水平复合。

积与余积：组合对象的两种方式

积和余积，积 (product) 在 Haskell 中对应的是 $p_1 = \texttt{fst},\ p_{2}=\texttt{snd}$，$a \times b = \texttt{(a, b)}$ 以及 $\left<f,\ g\right> = \mathtt{f\ \&\&\&\ g}$ 。注意，积特指笛卡尔积，是更一般的张量积 (tensor product, $\otimes$ ) 的特例。顺便介绍对偶的概念，将 $z,\ a,\ b,\ a \times b$ 的整张交换图反过来，就可以得到余积 $\{a+b,\ i_{1},\ i_{2}\}$，在 Haskell 中对应 $\{\mathtt{Either\ a\ b},\ \mathtt{Left},\ \mathtt{Right}\}$，态射映射为 $\left<f,\ g\right> = \mathtt{f\ |||\ g}$

极限与余极限（选读）

选读内容，极限 (limit) 与 余极限 (colimit)。我们所熟悉的终对象、始对象、积和余积在该定义下成为极限与余极限的特例。在 Haskell 中有终对象 () 以及对应的唯一态射族 const () :: a -> ()，作为对偶，还有始对象 Void 和对应的唯一态射族 absurd :: Void -> a。对于包含两个对象且无态射的图示，其极限为积，余极限为余积。

此外，对于图示中存在态射——即存在约束或相互作用——的情况，我们简要介绍等化子 (equalizer)、推出和拉回，同时提醒读者注意，由于 Haskell 中缺乏像 Idris 一样强大的依赖类型，我们难以在 $\mathcal H$ 中表达复杂的极限概念，这是 Haskell 类型系统的局限性。

幺半范畴

幺半范畴 (monoidal category)，结合子 $\alpha_{ABC}$ 以及左右单位子 $\lambda_A$ 和 $\rho_{A}$，它们都是自然变换，且满足由交换图给出的五边形公理和三角形公理。作为延申，提及 Mac Lane 严格性定理 (Mac Lane’s coherence theorem)，该定理告诉我们，定义中无需引入更复杂的交换图，只要满足三角形公理和五边形公理，任何由结合子与单位子组成的自然变换图都交换。

笛卡尔闭范畴

笛卡尔闭范畴 (Cartesian closed category, CCC)，大略上，拥有这种性质的范畴 $\mathcal C$，对于任何态射类 $\mathrm{Hom}_{\mathcal C}(A,\ B)$ ，都能找到相应的对象 $B^A \in \mathrm{Ob}(\mathcal C)$ 与之同构，即 $B^A \cong \mathrm{Hom}_{\mathcal C}(A,\ B)$。称 $B^A$ 为指数对象，它象征着 $\mathcal C$ 能够在其内部表示“从 $A$ 到 $B$ 所有态射”这个概念，而无需诉诸集合范畴 $\mathrm{Set}$。在 Haskell 中，指数对象 $B^A$ 恰是我们熟悉的函数类型签名 a -> b 。

我们经常听到在函数式语言中函数是一等公民，所谓“一等公民”，意思是说函数也是对象，自然也有自己的类型。现在我们看到，笛卡尔闭范畴正是“一等公民”的理论基础，它赋予了“一捆”态射作为对象的新身份，这也是一种新视角，是函数式语言强大表达能力的基石。

作为对比，延伸材料中简单提及对称幺半范畴 (symmetric monoidal category, SMC)，它比笛卡尔闭范畴更弱，用于建模资源有限的过程，在编程语言中对应线性类型。对称幺半范畴没有对角态射 $\Delta\ :\ A\to(A,\ A)$ 和丢弃态射 $!\ :\ A \to ()$，故所有类型无法复制无法丢弃，能且只能使用一次。

幺半群对象

幺半群对象 (monoid object)，特别强调，其幺半结构并非随意定义的，而是完全从该对象生活的幺半范畴中继承——大部分教程都没有重视这一点！那些有 SICP 基础的读者，熟悉 accumulate 的概念，更会想当然地认为：对象上的幺半结构是人工随意赋予的，是“一个点上局部的结构”，与来自范畴的宏观结构无关——这是严重狭隘和错误的认识！我们明确指出这一点，对下文中引入 Applicative 和 Monad 的概念非常有帮助。

准确地说，我们所熟悉的“幺半群”，其定义中要求一种二元运算，我们可以自由访问该运算的第一个参数和第二个参数——这仿佛是天经地义的废话。我们特别强调，对象之所以具有这种性质，绝非“免费”得来，而是继承了范畴的幺半结构——由 (,) 诱导的笛卡尔积幺半结构。为了深化理解，我们构造一个“反向”的世界，即通过 Either 诱导的余积幺半范畴，我们会在这种情形下观察幺半群对象的行为，它非常古怪，能给读者留下深刻印象。

弱幺半函子与 Applicative

弱幺半函子 (lax monoidal functor)，保持源范畴上的幺半结构，在 Haskell 中对应 Applicative，用于合并相互独立的子计算。数学家习惯的接口是 unit :: () -> f () 和 strength :: (f a, f b) -> f (a, b)，程序员习惯的接口是 pure 和 <*>，注意我们可以用 {fmap, unit, strength} 实现 {pure, <*>}，反之亦然，因此二者等价。

自函子范畴上的幺半群对象与 Monad

自函子范畴上的幺半群对象，“压平”嵌套的函子，在 Haskell 中对应单子 Monad，用于串联互相依赖的子计算。数学家习惯的接口是 unit :: a -> f a 和 join :: f f a -> f a，而程序员习惯的接口是 return / pure 和 >>=，同样，二者等价。作为延申，可以提一下 Kleisli 范畴与 Monad 的联系。

Freyd 范畴与 Arrow（选读）

选读内容，第一次阅读可跳过，Freyd 范畴和 Arrow，这是一种介于 Applicative 和 Monad 之间的抽象。

伴随函子

伴随函子 (adjoint functors)，两个自函子 $\mathfrak{f},\ \mathfrak{g}$ 伴随，记为 $\mathfrak{f} \dashv \mathfrak{g}$ ，这要求 $\mathrm{Hom}(\mathfrak{f}(a),\ b) \cong \mathrm{Hom}(a,\ \mathfrak{g}(b))$。

作为例子，可以证明 (->) s 是 (s, ) 的伴随，而证明所依赖的双射就是 curry 和 uncurry；恒等函子也是 Maybe 函子的伴随。作为伴随函子最有趣的性质，如果 $\mathfrak{f} \dashv \mathfrak{g}$，那么 $\mathfrak{g} \circ \mathfrak{f}$ 则“免费”生成一个 Monad，即我们自动从同构中得到两个自然变换，对单位变换有：

$$\mathtt{unit}_{X}\ :\ X\ \to\ \mathfrak{g} \circ \mathfrak{f}\ (X)$$

对“压平变换”有：

$$\mathtt{join}_{X}\ :\ (\mathfrak{g} \circ \mathfrak{f}) \circ (\mathfrak{g} \circ \mathfrak{f})\ (X) \to\ \mathfrak{g} \circ \mathfrak{f}\ (X)$$

我们也提供一些合成 Monad 的例子：积函子 (s, ) 与指数函子 (->) s 复合而成的 monad 是 (s, ) -> s ，在 Haskell 中称为 State monad，而恒等函子和 Maybe 函子生成的就是 Maybe monad；[] monad 也由类似的伴随函子生成而来。总而言之，伴随函子反映了函子间深刻的结构关联与优良的性质。在对偶情形下，用 $\mathfrak{f} \circ \mathfrak{g}$ 可以生成一个余单子 (comonad)，我们所熟悉的 State monad，其对偶的 comonad 是 (s, (->) s)，在 Haskell 中称为 Store comonad，也称 costate monad，下文中的 lens 库正是建立在这种结构上。

范畴论的世界观：实例研究

插入小节，本节尝试通过实例探讨范畴论的世界观，即“外部视角”。本节尝试构造一系列与 Bool 类型相关的态射和对象，实现了完整的逻辑运算。读者将会清晰地认识到，不依赖内部的“值视角”，而是转向外部的“态射视角”，我们同样可以还原 Bool 类型的全部行为，范畴论的抽象并没有丢失任何信息。核心构造：定义两个态射 true :: () -> Bool 和 false :: () -> Bool，加入 not :: Bool -> Bool、and :: (Bool, Bool) -> Bool 等态射，配合相应的交换图用以约束这些态射的行为。我们还介绍一种（思维观念上的）语法糖，即“值-类型” val :: a 可以看成范畴幺元 () 到对象 a 上的态射 val :: () -> a，在这种对应关系下，内部视角的“值”可以看作这种态射的唯一标识；类似地，可以将函数 f 加载实参 val 后的输出 f val :: b 看作态射复合 f . val :: () -> b，对多参数函数可以类似处理，不再赘述。在延伸内容中，可以额外提一提终对象 (terminal object) 和全局元素 (global element) 两个概念。

透镜与棱镜：解析 lens 库

Profunctor Optics 和 lens 库，Control.Lens.Prism，它是 Haskell 生态系统中最重要的工具，设计极尽工巧。此刻，读者已经掌握了足够的范畴论概念，本节中我们会展示这些概念的威力，全面剖析 lens 的设计思想和实现，我们会看到它事实上是一个 Costate comonad，源于指数对偶，任何笛卡尔闭范畴都能自动生成这样的 comonad。这也许是整份讲义中最优美、最普适的代数结构，我们期待本节内容能为读者带来审美和智识上的双重趣味。

米田引理

米田引理 (Yoneda lemma)，广义元素 (generalized element) ，依赖类型（Haskell 中不支持），本节是范畴论内容的最后一块拼图，也是这份讲义在形式上的结尾。

尾声：形式化的边界

尾声，选读内容：形式化的边界。上述内容让读者体会到了范畴论优雅而精密的结构，也见证了范畴论与 Haskell 语言相结合带来的强大抽象能力。但是，写在最后，读者请务必意识到，所谓 Hask 范畴并不是一个真正的范畴！

表面上看，这是因为 Haskell 语言的一些病态性质，例如底 (bottom，记为 $\bot$ ) 的存在，导致并非每个 Haskell 函数都能输出它所“承诺”的类型。一方面，使用偏函数会让我们很快感知到 $\bot$ 的影响，例如 head :: [a] -> a，当列表为空时它会报错，而非输出我们约定好的 a 类型；另一方面，即使我们避免使用偏函数——遵循 Haskell 社区的忠告——我们很快^[6]会意识到这并非一个简单的“编码规范”问题，绝不是你换成 safeHead :: [a] -> Maybe a 就能轻松绕行——事实上要深刻得多，它直接与停机问题相关。

哥德尔不完备定理说明，我们永远不可能把形式化推向极致，即便我们自信满满地通过 Maybe 或 Either 安置了所有异常，我们也许忽略了更基本的问题：我们的函数真的会停止吗？它能在有限的时间内输出一个我们约定的类型吗？谁负责证明？从停机问题——作为一切可计算问题的终点，也是形式化的终点——往回看，一个宏大的真相缓缓显出轮廓，即语言的表达能力和类型系统的精度在超过某个临界点后会相互制约。

现实中的编程语言必须在二者间找到平衡，这个话题还可以充分延伸下去，衔接到更为现代的函数式语言，例如 Idris 2 和 Lean 4，但那将远远超出这份讲义最初划定的概念边界。接下来的旅途，我们将方向盘交还给读者，读者已经掌握了所有必要的知识，接受了充分的训练，是时候开始一番激动人心的自由冒险了！

---

1. 此事在《人月神话》中亦有记载，一般作为“没有银弹”的补充说明。 ↩︎

2. 指 GPT 3.5 公开的时间点，在那之后，一切面向文本输入输出的工作都在日渐失去价值。这个说法最早可以追溯到知乎用户@酱紫君，我非常认同。 ↩︎

3. 除了库霸王，我似乎看不出有任何一个角色关心碧姬公主，我甚至怀疑，有些通关了很多代正作的人第一次知道碧姬公主是在《马里奥赛车》。 ↩︎

4. 由于我不是计算机系科班，而 SICP 是我的编程启蒙读物，导致 Scheme 甚至是我的母语——或者换句话说，我在启蒙阶段就是一个学杂了的双语者，Python 和 Scheme 都是我的母语。我无法确定 SICP 多大程度塑造了我今天的思维，那是我进入这个世界的第一扇门。十年前，我抬头看到门楣上刻着铭文，抽象与隔离，有一个声音一遍一遍问我准备好了吗，我迫不及待地推开那扇门，隆隆声扬起一阵呛人的灰尘，然后我意识到门后是什么——现实世界汹涌的复杂性。后来我逐渐明白，那铭文是一则咒语，我们用肉体凡胎试图理解——并对抗——比我们强大亿万倍的复杂性，那是唯一的法术。 ↩︎

5. 人的工作记忆大约只能容纳 $7 \pm 2$ 个区块 (chunks)，怎样组织区块的内容并控制区块的数量，这直接决定我们能处理多复杂的问题。 ↩︎

6. 出于巧合，某天你初次尝试定义某种“有限规模的容器”作为一个类型，你定义了若干操作，尝试让编译器帮你证明这些操作都保持你的容器有限。起初一帆风顺，但当你偶然写下某种递归操作，你突然察觉到编译器表现出一些怪异的行为，接着你开始反思，是不是你设计的类型定义有问题，也许你漏掉了什么——随着你反复迭代，你潜意识中怀疑一切背后也许有什么神秘的东西，似乎是某种你暂时说不清楚的限制，并非 Haskell 语言给你的限制，而是比那更宏大、更深刻、更接近某种事物的本源——你不知道如何表达这种感受，于是你开始搜集资料，终于，你看到了这份讲义。 ↩︎