<译>米田引理

上一篇：可表函子

原文地址：https://bartoszmilewski.com/2...

范畴论中的大多数构造都是其余具体数学领域的泛化。诸如积、余积、幺半群和指数等等，早都在范畴论之前被了解了。在不一样的数学分支中，它们也许有不一样的名字。集合论中的笛卡儿积，序数理论的下确界，逻辑中的连词——他们都是范畴积这样一个抽象观点的具体例子。

但做为一个有关范畴的通常陈述，米田引理却彻底不一样。它少有或没有其余数学分支中的先例。有些人说与它最靠近的类比是群论中的凯莱定理（每一个群都同构于某个集合的置换群）。

米田引理的设定是一个任意范畴C和一个从C到Set的函子F。咱们已经在以前的部分看到过一些指向Set的函子是可表的，也就是同构于一个hom函子。米田引理是说全部指向Set的函子都能经过天然变换从hom函子得到，并且米田引理精确的列举了全部这样的变换。

在讨论天然变换的时候，我曾说过天然性条件可能很是严格。当你定义一个天然变换在一个对象上的份量的时候，天然性得强到能够把这个份量“搬”到另外一个对象的份量上，而这另外一个对象和原对象有态射链接。源范畴和靶范畴的箭头越多，你要搬运天然变换的份量的限制就越多。Set碰巧就是一个箭头很是多的范畴。

米田引理告诉咱们，一个hom函子和任意其余函子F间的天然变换被它的单个份量在一个点的取值彻底决定！这个天然变换剩下的部分仅仅遵循天然性条件。

因此让咱们再来看看米田引理所用到的两个函子间的天然性条件吧。第一个函子是hom函子。它把C的任意对象x映为态射的集合C(a, x)——a是C中的一个固定对象。咱们也已经看到过它把任意x到y的态射f映为C(a, f)。

第二个函子是任意指向Set的函子F。

让咱们把这两个函子间的天然变换称做α。由于咱们是在Set中操做，像α_x或α_y这样的天然变换份量就只是常规的集合间的函数：

α_x :: C(a, x) -> F x
a_y :: C(a, y) -> F y

而由于这些都是函数，咱们就能够看看它们在具体点上的值。但集合C(a, x)里的点是什么？这就是关键的观察了：集合C(a, x)的每一个点也是个从a到x的态射h。

因此α的天然性四方图：

α_y ∘ C(a, f) = F f ∘ α_x

逐点做用在h上时，就变成了：

α_y (C(a, f) h) = F f (α_x h)

你能够从以前的部分回想起hom函子C(a, -)在态射f上的行为就被定义为前复合：

C(a, f) h = f ∘ h

这就导出了：

α_y (f ∘ h) = (F f) (α_x h)

这个条件究竟有多强看看让x等于a的情形就知道了。

这时h变成了一个从a到a的态射。咱们知道至少存在一个这样的态射，h = id_a。让咱们把它带入：

α_y f = (F f) (α_a id_a)

注意发生了什么：左边是α_y在C(a, y)的任意元素f上的做用。而且它由α_a在id_a的这单单一个值所彻底决定。咱们能够任意选取这样的值，这样就生成了一个天然变换。由于α_a的值落在集合F a中，因此F a的任意点都定义了某个α。

反过来，给定任意从C(a, -)到F的天然变换α，你能够计算出它在id_a的值，从而获得一个F a的点。

这样咱们就证实了米田引理：

从 C(a, -)到 F的天然变换和 F a的元素是一一对应的。

换句话说，

Nat(C(a, -), F) ≅ F a

或者说，若是咱们用记号[C, Set]表示C和Set间的函子范畴，天然变换的集合就只是这个范畴的一个hom集了，而且咱们能够写成：

[C, Set](C(a, -), F) ≅ F a

这个对应其实是个天然同构，我以后会解释这是怎么回事。

如今让咱们试着直观感觉下这个结果。最让人惊讶的莫过于整个天然变换从一个凝结点开始结晶了：凝结点就是天然变换做用于id_a的值。在天然性条件下，天然变换从该点向外延伸。它覆盖了Set中全部C的像。因此咱们首先考虑下C在C(a, -)的像。

让咱们从a本身的像开始。在hom函子C(a, -)下，a被映为集合C(a, a)。另外一方面，在函子F下，它被映为集合F a。天然变换的份量α_a是某个从C(a, a)到F a的函数。让咱们仅仅关注C(a, a)的一个点，也就是那个对应于态射id_a的点。为了强调它只是集合中的一个点，咱们把它叫作p。份量α_a应当把p映为F a的某个点q。我将给你证实任意q的选择会导出惟一的天然变换。

第一个断言是q的选择会惟一决定函数α_a的剩余部分。真的，让咱们任选C(a, a)的另外一个点p'，它对应某个从a到a的态射g。接下来就是米田引理的魔法时刻了：g能够被当作集合C(a, a)的某个点p',同时它还对应着两个集合间的函数。确实，在hom函子下，态射g被映为函数C(a, g)；在F下它被映为F g。

如今咱们考虑C(a, g)在咱们原始的p上的做用，p就是对应着id_a的那个家伙。这定义成前复合，g∘id_a，它就是g，也对应着咱们的点p'。因此态射g被映为了一个把p映为p'的函数，而p'就是g。咱们整整兜了一圈！

如今考虑F g在q上的做用。这会是某个q'，F a的一个点。为了补全天然四方图，p'必须在α_a下被映为q'。咱们选取了任意的p'(也就是任意的g)而后获得了它在α_a下的像，所以函数α_a彻底肯定了。

第二个断言是对于C中的任意和a有链接的对象x，α_x会被惟一决定。缘由是相似地，只不过如今咱们多了两个集合C(a, x)和F x，而且从a到x的态射g在hom函子下被映为了：

C(a, g) :: C(a, a) -> C(a, x)

而在F下被映为：

F g :: F a -> F x

一样地，C(a, g)在咱们的p上的做用由前复合给出：g ∘ id_a，这对应了C(a, x)的一个点p'。天然性决定了α_x做用在p'上的值会是：

q' = (F g) q

由于p'是任取的，因此所以整个α_x被肯定了。

若是C中有和a没有链接的对象呢？它们在C(a, -)下会通通被映为一个集合——空集。回忆一下，空集是集合范畴的初始对象。这意味着从它到任意其余集合只有一个函数。咱们曾把它叫作absurd。因此一样地，咱们仍然没有选择天然变换份量的余地：它只能是absurd。

一个理解米田引理的方法是把指向Set的函子间的天然变换们就看做一堆函数族，而函数一般是会损失信息的。一个函数可能会坍缩信息，而且它可能只覆盖上域的一部分。那些仅有的不会损失信息的函数就是那些可逆函数——同构。所以呢，最好的保持结构的指向Set的函子就是那些可表的。它们或者是hom函子，或者和hom函子天然同构。任何其余从hom函子获得函子F的过程都损失了信息。这样的变换可能不止损失了信息，它也可能只覆盖了函子F在Set上像的一小部分。

Hasekll中的米田引理

咱们已经遇到过Haskell中假装成reader函子的hom函子了：

type Reader a x = a -> x

reader经过前复合映射态射（这里就是函数）：

instance Functor (Reader a) where
    map f h = f . h

米田引理告诉咱们reader函子能够被天然地映为其余函子。

一个天然变换就是一个多态函数。因此给定一个函子F，咱们就有一个由reader函子到它的映射：

alpha :: forall x . (a -> x) -> F x

一般来讲，forall是能够省略的，但我想把它明确地写出来以强调天然变换的参数化多态性质。

米田引理告诉咱们这些天然变换和F a的元素们一一对应：

forall x . (a -> x) -> F x ≅ F a

这个等价的右边通常被看做一个数据结构。还记得把函子看做容器的推广的解释吗？F a是一个a的容器。但左边是个以一个函数做为参数的多态函数。米田引理说这两种表达等价——它们包含了一样地信息。

另外一个说法是：给我一个这种类型的多态函数：

alpha :: forall x . (a -> x) -> F x

我就能获得一个a的容器。技巧就是咱们以前在米田引理的证实中用到过的：咱们用id调用这个函数就获得了F a的一个元素：

alpha id :: F a

反过来也对。给定一个F a的值：

fa :: F a

就能够定义一个恰当类型的多态函数：

alpha h = fmap h fa

你能够轻易地在这两种表达间来回切换。

多种表达的好处是其中一种可能比另外一种易于复合，或者某些应用中一种可能比另外一种更有效率。

这个原理地最简单示例就是常常用在编译器构造中地编码转换：延继传递风格或CPS。这是米田引理在恒等函子上最简单的应用。把F换成恒等函子就获得了：

forall x . (a -> r) -> r ≅ a

关于延继传递风格（Continuation-passing style，CPS），网上的叫法不一，但大多把continuation译为“延续”，我以为不妥。由于在CPS中，把须要传递的类型为 (a -> r)的函数就叫the continuation。称呼一个函数为延续毕竟有些口语，不符合数学的习惯，因而我就自做主张的译为“延继”了。译者注。

这个公式的解释是任意类型a能够被代替成一个以一个a的“处理器”为参数的函数。一个处理器就是一个接受a为参数并执行后续计算的函数——延继。（类型r一般封装成某种类型的状态码）

这种编程风格在用户界面编程、异步系统和并行编程中都很是广泛。CPS的缺点是它设计了控制的反向。开发端和用户（处理器端）的代码是分离的，这就不易于复合。谁要是作过些通常的web编程，就会了解交互式状态处理程序的面条代码的噩梦了。就像咱们以后会看到的，若是函子和单子使用得当，就能存储一些CPS的可复合性质了。

逆米田引理

就像以往同样，咱们经过将箭头反向获得了额外的构造。米田引理能够应用到反范畴C_op从而给出逆变函子间的映射。

等价的说，咱们经过固定hom函子的靶对象而不是源对象获得了逆米田引理。咱们获得从C到Set的逆变hom函子：C(-, a)。米田引理的这个逆变版本构建了这个函子到其余任意逆变函子F间的天然变换与集合F a的元素之间的一一对应：

Nat(C(-, a), F) ≅ F a

这儿是逆米田引理Haskell版本：

forall x . (x -> a) -> F x ≅ F a

注意，有些文献中把这个逆变版本就叫米田引理。

挑战

1. 证实这两个在Haskell中组成米田同构的函子phi和psi互逆。

   phi :: (forall x . (a -> x) -> F x) -> F a
   phi alpha = alpha id

   psi :: F a -> (forall x . (a -> x) -> F x)
   psi fa h = fmap h fa

2. 所谓离散范畴就是指有一些对象，但除了恒等态射外没有别的态射的范畴。米田引理是如何处理从这个范畴出发的函子的？
3. unit的列表[()]除了它的长度不包含任何其余信息。因此，做为一个数据类型，它能够视为整数的一个编码方式。空列表表明0，单例列表[()](这是一个值，并非类型)表示1，等等。请使用米田引理构造出这个列表函子的另外一种表示。

参考文献

1. Catsters video

致谢

感谢Gershom Bazerman检查个人数学和逻辑，以及André van Meulebrouck在整个系列中的编辑上的帮助。

下一篇：米田嵌入