第 30 章：Lawvere 理论（Lawvere Theories）
原文：Bartosz Milewski, Category Theory for Programmers, Scala Edition, Chapter 30. 原书 PDF、
.tex源文件及相关图像采用 CC BY-SA 4.0；本译文按同一许可发布。
如今，如果谈函数式编程，就很难不提单子。但还有另一个平行宇宙：在那里，由于某种偶然，Eugenio Moggi 把注意力投向了 Lawvere 理论，而不是单子。让我们探索一下那个宇宙。
30.1 泛代数（Universal Algebra）
有很多方式可以在不同抽象层级上描述代数。我们试图找到一种通用语言，用来描述幺半群、群或环这类东西。在最简单的层次上，所有这些构造都定义了一些作用在集合元素上的运算，再加上一组这些运算必须满足的定律。比如，幺半群可以用一个满足结合律的二元运算来定义。它还有一个单位元素和单位律。不过稍微发挥一点想象力，就可以把单位元素变成一个零元运算，也就是一个不接收参数、返回集合中某个特殊元素的运算。
如果想谈论群，就要加入一个一元运算，它接收一个元素并返回它的逆元。与之配套的是左逆律和右逆律。环定义两个二元运算，再加上一些更多定律。如此等等。
整体图景是：一个代数由一组不同 n 值上的 n 元运算，以及一组等式恒等式定义。这些恒等式全部都是全称量化的。结合律方程必须对所有三个元素的可能组合成立，诸如此类。
顺便说一句，这会把域排除在考虑之外，原因很简单：零（加法单位元）没有乘法逆元。域的逆元律无法被全称量化。
如果用态射替换运算（函数），这个泛代数定义可以扩展到 Set 之外的范畴。我们不再选择一个集合，而是选择一个对象 a（称为泛对象）。一元运算只是 a 的自态射。那么其他元数怎么办？元数（arity）是给定运算的参数个数。二元运算（元数为 2）可以定义为从积 a x a 回到 a 的态射。一般的 n 元运算，是从 a 的 n 次幂到 a 的态射：
alpha_n :: a^n -> a
零元运算是从终对象（a 的零次幂）出发的态射。因此，为了定义任意代数，我们所需要的只是一个范畴，其对象是某个特殊对象 a 的各次幂。具体的代数被编码在这个范畴的 hom-set 中。概括来说，这就是 Lawvere 理论。
Lawvere 理论的推导会经过许多步骤，所以先给出路线图：
- 有限集合范畴
FinSet。 - 它的骨架
F。 - 它的对偶
F^op。 - Lawvere 理论
L：范畴Law中的一个对象。 - Lawvere 范畴的模型
M：范畴Mod(Law, Set)中的一个对象。
30.2 Lawvere 理论（Lawvere Theories）
所有 Lawvere 理论都有共同的骨架。Lawvere 理论中的所有对象，都通过积（实际只是幂）由一个对象生成。但在一般范畴中，我们如何定义这些积？事实证明，可以通过来自一个更简单范畴的映射来定义积。实际上，这个更简单的范畴可以定义余积而不是积，然后我们用一个反变函子把它们嵌入目标范畴。反变函子会把余积变成积，把内射变成投影。
作为 Lawvere 范畴骨架的自然选择，是有限集合范畴 FinSet。它包含空集 0、单元素集合 1、二元素集合 2，依此类推。这个范畴中的所有对象都可以由单元素集合通过余积生成（把空集看作零元余积的特殊情形）。例如，二元素集合是两个单元素集合的和，2 = 1 + 1，在 Haskell 中可以表达为：
type Two = Either () ()
在 Scala 中则是：
type Two = Either[Unit, Unit]
不过，即使自然地认为空集只有一个，单元素集合却可能有许多不同版本。特别是，集合 1 + 0 不同于集合 0 + 1，也不同于 1，虽然它们全都同构。集合范畴中的余积并不严格满足结合律。我们可以构造一个把所有同构集合都识别起来的范畴，从而修正这种情况。这样的范畴称为骨架。
换句话说，任意 Lawvere 理论的骨架都是 FinSet 的骨架 F。这个范畴中的对象可以用自然数（包括零）来识别，它们对应于 FinSet 中集合的元素个数。余积扮演加法的角色。F 中的态射对应于有限集合之间的函数。例如，从 0 到 n 有唯一态射（空集是初始对象），从 n 到 0 没有态射（除了 0 -> 0），从 1 到 n 有 n 个态射（内射），从 n 到 1 有一个态射，等等。这里，n 表示 F 中的一个对象，对应于 FinSet 中所有通过同构识别起来的 n 元集合。
利用范畴 F，可以把 Lawvere 理论形式化地定义为一个范畴 L，并配备一个特殊函子：
I_L :: F^op -> L
这个函子在对象上必须是双射，并且必须保持有限积（F^op 中的积与 F 中的余积相同）：
I_L(m x n) = I_L m x I_L n
有时你会看到这个函子被描述为对象上恒等（identity-on-objects），意思是 F 与 L 中的对象相同。因此我们会对它们使用相同名称，也就是用自然数表示它们。不过要记住，F 中的对象并不等同于集合（它们是同构集合的等价类）。
一般来说，L 中的 hom-set 比 F^op 中的 hom-set 更丰富。它们可以包含并不对应于 FinSet 中函数的态射（后者有时称为基本积运算）。Lawvere 理论中的等式定律编码在这些态射中。
关键观察是：F 中的单元素集合 1 会被映射到 L 中某个同样称为 1 的对象，而 L 中所有其他对象都会自动成为这个对象的幂。例如，F 中的二元素集合 2 是余积 1 + 1，所以它必须被映射到 L 中的积 1 x 1（或 1^2）。在这个意义上，范畴 F 的行为像是 L 的对数。
在 L 的态射中，有一部分是由函子 I_L 从 F 传递过来的。它们在 L 中扮演结构性角色。特别地，余积内射 i_k 会变成积投影 p_k。一个有用直觉是，把投影：
p_k :: 1^n -> 1
想象为某个 n 变量函数的原型：它忽略除了第 k 个变量之外的所有变量。反过来，F 中的常量态射 n -> 1 会变成 L 中的对角态射 1 -> 1^n。它们对应于变量复制。
L 中有趣的态射，是那些定义投影之外的 n 元运算的态射。正是这些态射区分了一个 Lawvere 理论与另一个 Lawvere 理论。它们是定义代数的乘法、加法、单位元素选择等等。不过，为了让 L 成为完整范畴，我们也需要复合运算 n -> m（或者等价地，1^n -> 1^m）。由于这个范畴结构简单，它们会成为更简单态射 n -> 1 的积。这是对一个语句的推广：返回积的函数就是一组函数的积；或者，正如我们之前见过的，hom-函子是连续的。
Lawvere 理论 L 基于 F^op，从中继承了那些定义积的“无趣”态射。它添加了描述 n 元运算的“有趣”态射（图中的虚线箭头）。
Lawvere 理论形成一个范畴 Law，其中态射是保持有限积并与函子 I 交换的函子。给定两个这样的理论 (L, I_L) 和 (L', I'_{L'})，它们之间的态射是函子 F :: L -> L'，满足：
F(m x n) = F m x F n
F . I_L = I'_{L'}
Lawvere 理论之间的态射封装了一种思想：把一个理论解释到另一个理论中。例如，如果忽略逆元，群乘法就可以解释为幺半群乘法。
最简单的平凡 Lawvere 范畴例子是 F^op 本身（对应于为 I_L 选择恒等函子）。这个没有运算也没有定律的 Lawvere 理论，恰好是 Law 中的初始对象。
此时如果能给出一个非平凡的 Lawvere 理论例子会很有帮助，但如果不先理解模型，解释起来会很困难。
30.3 Lawvere 理论的模型（Models of Lawvere Theories）
理解 Lawvere 理论的关键，是意识到一个这样的理论会概括许多共享同一结构的具体代数。例如，幺半群的 Lawvere 理论描述“成为幺半群”的本质。它必须对所有幺半群都有效。某个特定幺半群会成为这个理论的模型。
模型定义为从 Lawvere 理论 L 到集合范畴 Set 的函子。（Lawvere 理论也有使用其他范畴作为模型的推广，但这里我只关注 Set。）由于 L 的结构强烈依赖积，我们要求这样的函子保持有限积。因此，L 的一个模型，也称为 Lawvere 理论 L 上的代数，由下面这个函子定义：
M :: L -> Set
M(a x b) ~= M a x M b
注意，我们只要求在同构意义下保持积。这一点非常重要，因为严格保持积会排除大多数有趣理论。
模型保持积意味着，M 在 Set 中的像是一列由集合 M1 的幂生成的集合；M1 是 L 中对象 1 的像。我们把这个集合称为 a。（这个集合有时称为一个种类，sort；这种代数称为单种类代数。Lawvere 理论也可以推广到多种类代数。）特别地，来自 L 的二元运算会被映射为函数：
a x a -> a
和任何函子一样，L 中多个态射可能被压缩为 Set 中同一个函数。
顺便说一句，所有定律都是全称量化的等式，这意味着每个 Lawvere 理论都有一个平凡模型：一个常函子，把所有对象都映射到单元素集合，把所有态射都映射到其上的恒等函数。
L 中形如 m -> n 的一般态射会被映射为函数：
a^m -> a^n
如果有两个不同模型 M 和 N，它们之间的自然变换是一族以 n 为索引的函数：
mu_n :: M n -> N n
或者等价地：
mu_n :: a^n -> b^n
其中 b = N1。
注意，自然性条件保证了 n 元运算得到保持：
N f . mu_n = mu_1 . M f
其中 f :: n -> 1 是 L 中的一个 n 元运算。
定义模型的函子形成一个模型范畴 Mod(L, Set)，其中态射是自然变换。
考虑平凡 Lawvere 范畴 F^op 的一个模型。这样的模型完全由它在 1 上的值 M1 决定。由于 M1 可以是任意集合，这类模型与 Set 中的集合一样多。并且，Mod(F^op, Set) 中每个态射（函子 M 和 N 之间的自然变换）都由它在 M1 上的分量唯一决定。反过来，每个函数 M1 -> N1 都会诱导两个模型 M 与 N 之间的自然变换。因此，Mod(F^op, Set) 等价于 Set。
30.4 幺半群的理论（The Theory of Monoids）
Lawvere 理论最简单的非平凡例子描述幺半群结构。它是一个单一理论，提炼了所有可能幺半群的结构；其含义是，这个理论的模型张成了整个幺半群范畴 Mon。我们已经见过一个泛构造，它说明每个幺半群都可以从某个合适的自由幺半群出发，通过识别一部分态射获得。因此，单个自由幺半群已经概括了大量幺半群。不过，自由幺半群有无限多个。幺半群的 Lawvere 理论 LMon 把它们全部组合到一个优雅构造中。
每个幺半群都必须有单位元，所以在 LMon 中必须有一个特殊态射 eta，从 0 到 1。注意，在 F 中不可能有对应态射。这样的态射会走相反方向，从 1 到 0，也就是在 FinSet 中从单元素集合到空集的函数。这样的函数不存在。
接下来考虑态射 2 -> 1，也就是 LMon(2, 1) 的成员，它必须包含所有二元运算的原型。当在 Mod(LMon, Set) 中构造模型时，这些态射会被映射为从笛卡尔积 M1 x M1 到 M1 的函数。换句话说，它们是双参数函数。
问题是：只使用幺半群运算符，可以实现多少个双参数函数？把两个参数称为 a 和 b。有一个函数会忽略两个参数并返回幺半群单位元。接着有两个投影，分别返回 a 和 b。随后还有返回 ab、ba、aa、bb、aab 等等的函数。事实上，这样的双参数函数与由生成元 a 和 b 构成的自由幺半群中的元素一样多。注意，LMon(2, 1) 必须包含所有这些态射，因为其中一个模型就是自由幺半群。在自由幺半群中，它们对应于彼此不同的函数。其他模型可能把 LMon(2, 1) 中多个态射压缩为一个函数，但自由幺半群不会。
如果把具有 n 个生成元的自由幺半群记作 n*，就可以把 hom-set L(2, 1) 与 Mon（幺半群范畴）中的 hom-set Mon(1*, 2*) 识别起来。一般来说，我们选择 LMon(m, n) 为 Mon(n*, m*)。换句话说，范畴 LMon 是自由幺半群范畴的对偶。
幺半群 Lawvere 理论的模型范畴 Mod(LMon, Set) 等价于所有幺半群构成的范畴 Mon。
30.5 Lawvere 理论与单子（Lawvere Theories and Monads）
你可能还记得，代数理论可以用单子来描述，特别是用单子的代数来描述。因此，Lawvere 理论与单子之间存在联系并不令人意外。
首先看看 Lawvere 理论如何诱导一个单子。它通过遗忘函子和自由函子之间的伴随来做到这一点。遗忘函子 U 会为每个模型指派一个集合。这个集合由把 Mod(L, Set) 中的函子 M 作用到 L 中对象 1 上得到。
还可以利用 F^op 是 Law 中初始对象这个事实来推导 U。这意味着，对于任意 Lawvere 理论 L，都有唯一函子 F^op -> L。由于模型是从理论到集合的函子，这个函子会在模型上诱导反方向函子：
Mod(L, Set) -> Mod(F^op, Set)
但正如前面讨论过的，F^op 的模型范畴等价于 Set，因此得到遗忘函子：
U :: Mod(L, Set) -> Set
可以证明，如此定义的 U 总是有一个左伴随，也就是自由函子 F。
对有限集合来说，这一点很容易看出。自由函子 F 生成自由代数。自由代数是 Mod(L, Set) 中的一个特定模型，它由一个包含 n 个生成元的有限集合生成。我们可以把 F 实现为可表示函子：
L(n, -) :: L -> Set
为了说明它确实是自由的，只需要证明它是遗忘函子的左伴随：
Mod(L(n, -), M) ~= Set(n, U(M))
先化简右侧：
Set(n, U(M)) ~= Set(n, M1) ~= (M1)^n ~= M n
这里我使用了这样一个事实：态射集合同构于指数对象；在这个例子中，它只是迭代积。这个伴随来自 Yoneda 引理：
[L, Set](L(n, -), M) ~= M n
遗忘函子和自由函子一起，在 Set 上定义了单子 T = U . F。因此，每个 Lawvere 理论都会生成一个单子。
事实证明，这个单子的代数范畴等价于模型范畴。
你可能记得，单子代数定义了对用单子形成的表达式进行求值的方式。Lawvere 理论定义了可用于生成表达式的 n 元运算。模型提供了对这些表达式求值的手段。
不过，单子与 Lawvere 理论之间的联系并不是双向无条件成立的。只有有限型单子才会导向 Lawvere 理论。有限型单子基于有限型函子。Set 上的有限型函子完全由它在有限集合上的作用决定。它在任意集合 a 上的作用可以用下面的余端求值：
F a = ∫^n a^n x (F n)
由于余端推广了余积或和，这个公式可以看成幂级数展开的推广。或者也可以使用这样的直觉：函子是一种广义容器。在这种情况下，装有 a 的有限型容器可以描述为形状与内容的和。这里，F n 是用于存储 n 个元素的形状集合，而内容是一个 n 元组，本身是 a^n 的一个元素。例如，列表（作为函子）是有限型的，每种元数都有一个形状。树在每种元数上有更多形状，等等。
首先，所有由 Lawvere 理论生成的单子都是有限型的，并且可以表达为余端：
T_L a = ∫^n a^n x L(n, 1)
反过来，给定 Set 上任意有限型单子 T，我们可以构造一个 Lawvere 理论。我们从为 T 构造 Kleisli 范畴开始。你可能还记得，在 Kleisli 范畴中，从 a 到 b 的态射由底层范畴中的态射给出：
a -> T b
限制到有限集合时，这变成：
m -> T n
这个 Kleisli 范畴的对偶 Kl_T^op，再限制到有限集合上，就是所需的 Lawvere 理论。特别地，描述 L 中 n 元运算的 hom-set L(n, 1)，由 hom-set Kl_T(1, n) 给出。
事实证明，我们在编程中遇到的大多数单子都是有限型的，显著例外是 continuation 单子。Lawvere 理论的概念也可以扩展到有限型运算之外。
30.6 作为余端的单子（Monads as Coends）
让我们更详细地考察这个余端公式。
T_L a = ∫^n a^n x L(n, 1)
首先，这个余端取自 F 中定义的一个 profunctor P：
P n m = a^n x L(m, 1)
这个 profunctor 在第一个参数 n 上是反变的。考虑它如何提升态射。FinSet 中的一个态射是有限集合之间的映射：
f :: m -> n
这样的映射描述了从一个 n 元集合中选取 m 个元素（允许重复）。它可以被提升为 a 的幂之间的映射，也就是（注意方向）：
a^n -> a^m
这种提升只是从 n 元组 (a1, a2, ... an) 中选取 m 个元素（可能带重复）。
例如，取 f_k :: 1 -> n，也就是从 n 元集合中选择第 k 个元素。它会提升为一个函数，接收 a 的 n 元组并返回第 k 个元素。
或者，取 f :: m -> 1，也就是把所有 m 个元素都映射到同一个元素的常量函数。它的提升是一个函数，接收 a 的单个元素并把它复制 m 次：
x -> (x, x, ... , x)
你可能注意到，相关 profunctor 在第二个参数上协变这一点并非立刻显然。hom-函子 L(m, 1) 实际上在 m 上是反变的。不过，我们取余端的范畴不是 L，而是 F。余端变量 n 遍历有限集合（或这些集合的骨架）。范畴 L 包含 F 的对偶，所以 F 中的态射 m -> n 是 L 中 L(n, m) 的成员（嵌入由函子 I_L 给出）。
来检查 L(m, 1) 作为从 F 到 Set 的函子的函子性。我们想提升一个函数 f :: m -> n，因此目标是实现从 L(m, 1) 到 L(n, 1) 的函数。对应于函数 f，L 中有一个从 n 到 m 的态射（注意方向）。把这个态射前组合到 L(m, 1) 中，就得到 L(n, 1) 的一个子集。
注意，通过提升函数 1 -> n，我们可以从 L(1, 1) 到达 L(n, 1)。稍后会用到这个事实。
反变函子 a^n 与协变函子 L(m, 1) 的积，是一个 profunctor F^op x F -> Set。记住，余端可以定义为 profunctor 所有对角成员的余积（不交和），再识别其中某些元素。这些识别对应于 cowedge 条件。
这里，余端一开始是所有 n 上集合 a^n x L(n, 1) 的不交和。可以通过把余端表示为一个余等化子来生成这些识别。我们从离对角项 a^n x L(m, 1) 开始。为了到达对角线，可以把态射 f :: m -> n 作用到积的第一个分量，也可以作用到第二个分量。随后这两个结果会被识别。
a^n x L(m, 1) --<f,id>--> a^m x L(m, 1)
a^n x L(m, 1) --<id,f>--> a^n x L(n, 1)
我之前展示过，提升 f :: 1 -> n 会得到两个变换：
a^n -> a
以及：
L(1, 1) -> L(n, 1)
因此，从 a^n x L(1, 1) 出发，在提升 <f, id> 时可以到达：
a x L(1, 1)
而在提升 <id, f> 时可以到达：
a^n x L(n, 1)
不过，这并不意味着 a^n x L(n, 1) 的所有元素都可以与 a x L(1, 1) 识别起来。原因是，并非 L(n, 1) 的所有元素都能从 L(1, 1) 到达。记住，我们只能提升来自 F 的态射。L 中非平凡的 n 元运算无法通过提升态射 f :: 1 -> n 构造出来。
换句话说，在余端公式中，我们只能识别那些通过应用基本态射、能从 L(1, 1) 到达 L(n, 1) 的加项。它们全部等价于 a x L(1, 1)。基本态射就是 F 中态射的像。
来看 Lawvere 理论最简单的情形，也就是 F^op 本身。在这样的理论中，每个 L(n, 1) 都能从 L(1, 1) 到达。这是因为 L(1, 1) 是只包含恒等态射的单元素集合，而 L(n, 1) 只包含对应于 F 中内射 1 -> n 的态射，也就是基本态射。因此，余积中的所有加项都是等价的，于是得到：
T a = a x L(1, 1) = a
这就是恒等单子。
30.7 副作用的 Lawvere 理论（Lawvere Theory of Side Effects）
既然单子与 Lawvere 理论之间有这么强的联系，自然会问：Lawvere 理论能否在编程中作为单子的替代方案？单子的主要问题是它们不能很好地组合。构造单子变换器没有通用配方。Lawvere 理论在这方面有优势：它们可以用余积和张量积组合。另一方面，只有有限型单子才能轻易转换成 Lawvere 理论。这里的异常者是 continuation 单子。这个方向仍有研究在进行（见参考阅读）。
为了让你感受一下 Lawvere 理论如何用于描述副作用，我会讨论异常这个简单例子；传统上，它们使用 Maybe 单子实现。
Maybe 单子由带有单个零元运算 0 -> 1 的 Lawvere 理论生成。这个理论的模型是一个函子，它把 1 映射到某个集合 a，并把零元运算映射到一个函数：
raise :: () -> a
在 Scala 中：
def raise: Unit => A
可以用余端公式恢复 Maybe 单子。考虑加入零元运算对 hom-set L(n, 1) 做了什么。除了创建新的 L(0, 1)（它在 F^op 中不存在），它还会向 L(n, 1) 添加新的态射。这些态射是把形如 n -> 0 的态射与我们的 0 -> 1 组合得到的结果。在余端公式中，这些贡献都会与 a^0 x L(0, 1) 识别起来，因为它们可以从：
a^n x L(0, 1)
出发，通过两种不同方式提升 0 -> n 得到。
a^n x L(0, 1) --<f,id>--> a^0 x L(0, 1)
a^n x L(0, 1) --<id,f>--> a^n x L(n, 1)
这个余端化简为：
T_L a = a^0 + a^1
或者用 Haskell 记法：
type Maybe a = Either () a
Scala 中则是：
type Option[A] = Either[Unit, A]
它等价于：
data Maybe a = Nothing | Just a
Scala 中：
sealed trait Option[+A]
case object None extends Option[Nothing]
case class Some[A](a: A) extends Option[A]
注意，这个 Lawvere 理论只支持抛出异常，不支持处理异常。
30.8 挑战（Challenges）
- 枚举
F（FinSet的骨架）中2和3之间的所有态射。 - 证明幺半群 Lawvere 理论的模型范畴等价于 list 单子的单子代数范畴。
- 幺半群的 Lawvere 理论生成 list 单子。证明它的二元运算可以用相应的 Kleisli 箭头生成。
FinSet是Set的子范畴，并且存在一个把它嵌入Set的函子。Set上任意函子都可以限制到FinSet。证明有限型函子是其自身限制的左 Kan 扩张。
30.9 延伸阅读（Further Reading）
- F. William Lawvere, Functorial Semantics of Algebraic Theories
- Gordon Plotkin and John Power, Notions of computation determine monads