第 26 章：端与余端（Ends and Coends）
原文：Bartosz Milewski, Category Theory for Programmers, Scala Edition, Chapter 26. 原书 PDF、
.tex源文件及相关图像采用 CC BY-SA 4.0；本译文按同一许可发布。
我们可以给范畴中的态射附上许多直觉，但至少可以同意一点：如果有一个从对象 a 到对象 b 的态射，那么这两个对象在某种意义上是“相关的”。态射在某种意义上是这种关系的证明。在任意偏序范畴中，这一点尤其清楚：态射就是一种关系。一般来说，两个对象之间的同一关系可能有许多“证明”。这些证明形成一个集合，我们称为 hom-set。当对象变化时，就得到一个从对象 pair 到“证明”集合的映射。这个映射是函子性的：在第一个参数上逆变，在第二个参数上协变。可以把它看作建立了范畴中对象之间的全局关系。这个关系由 hom-函子描述：
C(-, =) :: C^op x C -> Set
一般来说，任何这样的函子都可以解释为在一个范畴的对象之间建立关系。关系也可以涉及两个不同范畴 C 和 D。描述这种关系的函子具有下面的签名，称为 profunctor：
p :: D^op x C -> Set
数学家说，这是一个从 C 到 D 的 profunctor（注意方向反了），并用带斜杠的箭头表示：
C ↛ D
可以把 profunctor 想成 C 的对象与 D 的对象之间的一种 proof-relevant relation，也就是携带证明的关系，其中集合中的元素象征这种关系的证明。只要 p a b 为空，a 与 b 之间就没有关系。请记住，关系不必是对称的。
另一个有用直觉，是把“自函子是容器”的想法推广开来。类型为 p a b 的 profunctor 值可以看作一个装有 b 的容器，而这个容器由类型为 a 的元素作为键来索引。特别地，hom-profunctor 的一个元素就是从 a 到 b 的函数。
在 Haskell 中，profunctor 被定义为一个双参数类型构造器 p，配有一个叫 dimap 的方法。dimap 会提升一对函数，其中第一个函数朝“错误”的方向：
class Profunctor p where
dimap :: (c -> a) -> (b -> d) -> p a b -> p c d
trait Profunctor[P[_, _]] {
def dimap[A, B, C, D]
(f: C => A)(g: B => D)(pab: P[A, B]): P[C, D]
}
profunctor 的函子性告诉我们：如果有一个证明说明 a 与 b 相关，那么只要存在一个从 c 到 a 的态射，以及另一个从 b 到 d 的态射，就能得到 c 与 d 相关的证明。或者，也可以把第一个函数看成把新键翻译为旧键，把第二个函数看成修改容器内容。
对于作用在同一个范畴内的 profunctor，可以从类型 p a a 的对角元素中提取大量信息。只要有一对态射 b -> a 和 a -> c，就可以证明 b 与 c 相关。更好的是，可以用单个态射抵达非对角值。例如，如果有态射 f :: a -> b，就可以提升 pair <f, id_b>，从 p b b 到 p a b：
dimap f id (p b b) :: p a b
dimap(f)(identity[B])(pbb): P[A, B]
或者，可以提升 pair <id_a, f>，从 p a a 到 p a b：
dimap id f (p a a) :: p a b
dimap(identity[A])(f)(paa): P[A, B]
26.1 双自然变换（Dinatural Transformations）
由于 profunctor 是函子，我们可以用标准方式定义它们之间的自然变换。不过，在许多情况下，只定义两个 profunctor 的对角元素之间的映射就够了。如果这样的变换满足反映两种连接对角元素到非对角元素方式的交换条件，它就称为双自然变换。
设 p 和 q 是函子范畴 [C^op x C, Set] 的成员。它们之间的双自然变换是一族态射：
alpha_a :: p a a -> q a a
对任意 f :: a -> b，下面的图都交换：
注意，这比自然性条件严格弱。如果 alpha 是 [C^op x C, Set] 中的自然变换，那么上图可以由两个自然性方块以及一个函子性条件构成（也就是 profunctor q 保持组合）：
注意，自然变换 alpha 在 [C^op x C, Set] 中的分量由一对对象索引，也就是 alpha_ab。另一方面，双自然变换只由一个对象索引，因为它只映射相应 profunctor 的对角元素。
26.2 端（Ends）
现在我们准备从“代数”推进到可以被认为是范畴论“微积分”的东西。端与余端的演算借用了传统微积分中的一些想法，甚至一些记法。特别地，余端可以理解为无限和或积分，而端类似无限积。甚至还有某种类似 Dirac delta 函数的东西。
端是极限的推广，其中函子被替换为 profunctor。我们不再有锥，而是有楔。楔的底部由 profunctor p 的对角元素构成。楔的顶点是一个对象（这里是一个集合，因为我们考虑的是取值于 Set 的 profunctor），边是一族把顶点映射到底部各集合的函数。可以把这一族函数想成一个多态函数，也就是在返回类型上多态的函数：
alpha :: forall a. apex -> p a a
在楔中，不像锥那样有连接底部顶点的函数。不过，正如前面看到的，给定 C 中任意态射 f :: a -> b，就可以把 p a a 和 p b b 都连接到公共集合 p a b。因此，我们要求下面的图交换：
这称为楔条件。它可以写成：
p id_a f . alpha_a = p f id_b . alpha_b
或者用 Haskell 记法写成：
dimap id f . alpha = dimap f id . alpha
(dimap(identity[A])(f) _ compose alpha) ==
(dimap(f)(identity[B]) _ compose alpha)
现在可以继续做泛构造，把 p 的端定义为泛楔：一个集合 e，以及一族函数 pi，使得对于任意另一个顶点为 a、边族为 alpha 的楔，都存在唯一函数 h :: a -> e，使所有三角形交换：
pi_a . h = alpha_a
端的符号是积分号，并把“积分变量”放在下标位置：
∫_c p c c
pi 的分量称为端的投影映射：
pi_a :: ∫_c p c c -> p a a
注意，如果 C 是离散范畴（除了恒等态射之外没有态射），那么端就是 p 在整个范畴 C 上所有对角项的全局积。稍后我会说明，在更一般的情况下，端与这个积之间通过 equalizer 存在关系。
在 Haskell 中，端公式会直接翻译成全称量词：
forall a. p a a
// no Rank-N types in Scala
// have to introduce a polymorphic function
trait PolyFunction1[P[_, _]] {
def apply[A](): P[A, A]
}
严格说，这只是 p 的所有对角元素的积，但由于参数性，楔条件会自动满足1。对于任意函数 f :: a -> b，楔条件读作：
dimap f id . pi = dimap id f . pi
(dimap(f)(identity[B]) _ compose pi.apply) ==
(dimap(identity[A])(f) _ compose pi.apply)
或者加上类型标注：
dimap f idb . pib = dimap ida f . pia
等式两边都具有下面的类型：
Profunctor p => (forall c. p c c) -> p a b
def side[P[_, _]: Profunctor]: PolyFunction1[P] => P[A, B]
其中 pi 是多态投影：
pi :: Profunctor p => forall c. (forall a. p a a) -> p c c
pi e = e
// no Rank-N types in Scala
// need a higher rank polymorphic function
trait PolyFunction2[P[_, _]] {
def apply[C](in: PolyFunction1[P]): P[C, C]
}
def pi[P[_, _]](implicit P: Profunctor[P]): PolyFunction2[P] =
new PolyFunction2[P] {
def apply[C](in: PolyFunction1[P]): P[C, C] =
in()
}
这里，类型推断会自动选择 e 的正确分量。
正如可以把锥的整组交换条件表达为一个自然变换，也可以把所有楔条件组织成一个双自然变换。为此，需要把常函子 Delta_c 推广为常 profunctor：它把所有对象 pair 映射到同一个对象 c，并把所有态射 pair 映射到该对象上的恒等态射。楔就是从这个函子到 profunctor p 的双自然变换。确实，当我们意识到 Delta_c 会把所有态射提升成同一个恒等函数时，双自然性六边形就缩小成楔菱形。
端也可以定义到 Set 以外的目标范畴中，但这里我们只考虑取值于 Set 的 profunctor 及其端。
26.3 作为 Equalizer 的端（Ends as Equalizers）
端定义中的交换条件可以用 equalizer 写出。首先定义两个函数（我使用 Haskell 记法，因为数学记法在这里似乎没那么友好）。这两个函数对应楔条件中汇合的两条分支：
lambda :: Profunctor p => p a a -> (a -> b) -> p a b
lambda paa f = dimap id f paa
rho :: Profunctor p => p b b -> (a -> b) -> p a b
rho pbb f = dimap f id pbb
def lambda[A, B, P[_, _]](P: Profunctor[P]): P[A, A] => (A => B) => P[A, B] =
paa => f => P.dimap(identity[A])(f)(paa)
def rho[A, B, P[_, _]](P: Profunctor[P]): P[B, B] => (A => B) => P[A, B] =
pbb => f => P.dimap(f)(identity[B])(pbb)
两个函数都把 profunctor p 的对角元素映射到下面这种类型的多态函数：
type ProdP p = forall a b. (a -> b) -> p a b
trait ProdP[P[_, _]] {
def apply[A, B](f: A => B): P[A, B]
}
这些函数类型不同。不过，如果形成一个巨大的积类型，把 p 的所有对角元素收集在一起，就可以统一它们的类型：
newtype DiaProd p = DiaProd (forall a. p a a)
case class DiaProd[P[_, _]](paa: PolyFunction1[P])
函数 lambda 和 rho 会诱导出从这个积类型出发的两个映射：
lambdaP :: Profunctor p => DiaProd p -> ProdP p
lambdaP (DiaProd paa) = lambda paa
rhoP :: Profunctor p => DiaProd p -> ProdP p
rhoP (DiaProd pbb) = rho pbb
def lambdaP[P[_, _]](P: Profunctor[P]): DiaProd[P] => ProdP[P] = {
case DiaProd(paa) =>
new ProdP[P] {
def apply[A, B](f: A => B): P[A, B] =
lambda(P)(paa[A])(f)
}
}
def rhoP[P[_, _]](P: Profunctor[P]): DiaProd[P] => ProdP[P] = {
case DiaProd(paa) =>
new ProdP[P] {
def apply[A, B](f: A => B): P[A, B] =
rho(P)(paa[B])(f)
}
}
p 的端就是这两个函数的 equalizer。记住，equalizer 会选出让两个函数相等的最大子集。在这里，它选出的就是所有对角元素之积中的一个子集；在这个子集中，楔图都会交换。
26.4 作为端的自然变换（Natural Transformations as Ends）
端最重要的例子是自然变换集合。两个函子 F 和 G 之间的自然变换，是从形如 C(F a, G a) 的 hom-set 中选出的一族态射。如果没有自然性条件，自然变换集合就只是所有这些 hom-set 的积。事实上，在 Haskell 中就是：
forall a. f a -> g a
// Yet another type needs to be introduced.
// To read more about FunctionK (~>):
// typelevel.org/cats/datatypes/functionk.html
trait ~>[F[_], G[_]] {
def apply[B](fa: F[B]): G[B]
}
F ~> G
它在 Haskell 中可行，是因为自然性来自参数性。不过在 Haskell 之外，穿过这些 hom-set 的并非所有对角截面都会产生自然变换。请注意，映射：
<a, b> -> C(F a, G b)
是一个 profunctor，因此研究它的端是有意义的。这是楔条件：
从集合 ∫_c C(F c, G c) 中选取一个元素。两个投影会把这个元素映射到某个特定变换的两个分量，把它们称为：
tau_a :: F a -> G a
tau_b :: F b -> G b
在左分支中，我们使用 hom-函子提升一对态射 <id_a, G f>。你也许记得，这种提升实现为同时前组合和后组合。当作用在 tau_a 上时，这个提升后的 pair 给出：
G f . tau_a . id_a
图的另一条分支给出：
id_b . tau_b . F f
楔条件要求二者相等，这正是 tau 的自然性条件。
26.5 余端（Coends）
如预期，端的对偶称为余端。它从楔的对偶构造出来，这个对偶叫余楔（cowedge，读作 co-wedge）。
余端的符号是积分号，并把“积分变量”放在上标位置：
∫^c p c c
正如端与积相关，余端与余积或和相关（在这个意义上，它类似积分，积分是和的极限）。这里没有投影，而是有从 profunctor 的对角元素向下进入余端的注入。如果没有余楔条件，就可以说 profunctor p 的余端要么是 p a a，要么是 p b b，要么是 p c c，依此类推。或者可以说，存在某个 a，使余端正是集合 p a a。定义端时使用的全称量词，在余端中变成存在量词。
所以，在伪 Haskell 中，会把余端定义为：
exists a. p a a
在 Haskell 中编码存在量词的标准方式，是使用全称量化的数据构造器。因此可以定义：
data Coend p = forall a. Coend (p a a)
trait Coend[P[_, _]] {
def paa[A]: P[A, A]
}
背后的逻辑是：应该可以用族类型 p a a 中任意一个值来构造余端，不管我们选择了哪个 a。
正如端可以用 equalizer 定义，余端也可以用 coequalizer 描述。所有余楔条件可以通过取 p a b 的一个巨大余积来概括，其中包含所有可能的函数 b -> a。在 Haskell 中，这会表达为存在类型：
data SumP p = forall a b. SumP (b -> a) (p a b)
trait SumP[P[_, _]] {
def f[A, B]: B => A
def pab[A, B]: P[A, B]
}
有两种方式可以求值这个和类型：用 dimap 提升函数，并把它应用到 profunctor p：
lambda, rho :: Profunctor p => SumP p -> DiagSum p
lambda (SumP f pab) = DiagSum (dimap f id pab)
rho (SumP f pab) = DiagSum (dimap id f pab)
def lambda[P[_, _]](P: Profunctor[P]): SumP[P] => DiagSum[P] =
sump => new DiagSum[P] {
def paa[A]: P[A, A] =
P.dimap(sump.f)(identity[A])(sump.pab)
}
def rho[P[_, _]](P: Profunctor[P]): SumP[P] => DiagSum[P] =
sump => new DiagSum[P] {
def paa[A]: P[A, A] =
P.dimap(identity[A])(sump.f)(sump.pab)
}
其中 DiagSum 是 p 的对角元素之和：
data DiagSum p = forall a. DiagSum (p a a)
trait DiagSum[P[_, _]]{
def paa[A]: P[A, A]
}
这两个函数的 coequalizer 就是余端。coequalizer 从 DiagSum p 得到，方式是识别那些由同一个参数应用 lambda 或 rho 得到的值。这里的参数是由一个函数 b -> a 和一个 p a b 的元素组成的 pair。应用 lambda 和 rho 会产生两个可能不同的 DiagSum p 类型值。在余端中，这两个值会被识别，从而自动满足余楔条件。
在集合中识别相关元素的过程，形式上称为取商。定义商需要一个等价关系 ~，它是自反、对称且传递的关系：
a ~ a
if a ~ b then b ~ a
if a ~ b and b ~ c then a ~ c
这样的关系会把集合分成等价类。每个等价类由彼此相关的元素组成。通过从每个类中选出一个代表，形成商集。一个经典例子是把有理数定义为整数 pair，并带有下面的等价关系：
(a, b) ~ (c, d) iff a * d = b * c
很容易检查这是一个等价关系。pair (a, b) 被解释为分数 a / b，而分子和分母有公因子的分数会被识别。有理数就是这些分数的等价类。
你也许还记得我们之前讨论极限和余极限时提到过，hom-函子是连续的，也就是说它保持极限。对偶地，逆变 hom-函子会把余极限转换为极限。这些性质可以推广到端和余端；端和余端分别是极限和余极限的推广。特别地，我们得到一个非常有用的恒等式，可以把余端转换成端：
Set(∫^x p x x, c) ~= ∫_x Set(p x x, c)
用伪 Haskell 看看它：
(exists x. p x x) -> c ≅ forall x. p x x -> c
它告诉我们，一个接收存在类型的函数等价于一个多态函数。这很合理，因为这样的函数必须准备好处理可能编码进存在类型中的任意一种类型。这与另一个原则相同：接收和类型的函数必须实现为 case 语句，也就是一组处理器的元组，和类型中出现的每种类型各有一个处理器。在这里，和类型被余端替换，而处理器族变成了端，也就是多态函数。
26.6 Ninja Yoneda 引理（Ninja Yoneda Lemma）
Yoneda 引理中出现的自然变换集合可以用端编码，得到下面这种表述：
∫_z Set(C(a, z), F z) ~= F a
还有一个对偶公式：
∫^z C(z, a) x F z ~= F a
这个恒等式强烈让人想起 Dirac delta 函数的公式（函数 delta(a - z)，或者更准确地说是一个分布，它在 a = z 处有一个无限峰值）。这里，hom-函子扮演 delta 函数的角色。这两个恒等式有时合称为 Ninja Yoneda 引理。
为了证明第二个公式，我们将使用 Yoneda 嵌入的一个推论：两个对象同构，当且仅当它们的 hom-函子同构。换句话说，a ~= b 当且仅当存在一个下面这种类型的自然变换，并且它是一个同构：
[C, Set](C(a, -), C(b, =))
从我们想要证明的恒等式左侧开始，把它放进一个到任意对象 c 的 hom-函子中：
Set(∫^z C(z, a) x F z, c)
使用连续性论证，可以把余端替换为端：
∫_z Set(C(z, a) x F z, c)
现在可以利用积与指数之间的伴随：
∫_z Set(C(z, a), c^(F z))
可以使用 Yoneda 引理“执行积分”，得到：
c^(F a)
（注意，我们使用了 Yoneda 引理的逆变版本，因为函子 c^(F z) 在 z 上是逆变的。）这个指数对象同构于 hom-set：
Set(F a, c)
最后，利用 Yoneda 嵌入，得到同构：
∫^z C(z, a) x F z ~= F a
26.7 Profunctor 组合（Profunctor Composition）
让我们进一步探索 profunctor 描述关系的想法；更精确地说，它描述 proof-relevant relation，也就是说集合 p a b 表示 a 与 b 相关的证明集合。如果有两个关系 p 和 q，就可以尝试组合它们。我们会说，如果存在某个中介对象 c，使得 q b c 和 p c a 都非空，那么 a 通过 q 在 p 之后的组合与 b 相关。这个新关系的证明是各个关系证明的所有 pair。因此，在理解存在量词对应余端、两个集合的笛卡尔积对应“证明的 pair”之后，可以用下面的公式定义 profunctor 的组合：
(q . p) a b = ∫^c p c a x q b c
下面是 Data.Profunctor.Composition 中等价的 Haskell 定义，做了一些重命名：
data Procompose q p a b where
Procompose :: q a c -> p c b -> Procompose q p a b
trait Procompose[Q[_, _], P[_, _], A, B]
object Procompose{
def apply[Q[_, _], P[_, _], A, B, C]
(qac: Q[A, C])(pcb: P[C, B]): Procompose[Q, P, A, B] = ???
}
这里使用了广义代数数据类型，也就是 GADT 语法，其中自由类型变量（这里是 c）会自动被存在量化。因此，未柯里化的数据构造器 Procompose 等价于：
exists c. (q a c, p c b)
这样定义的组合，其单位是 hom-函子；这直接来自 Ninja Yoneda 引理。因此，有理由追问：是否存在一个以 profunctor 作为态射的范畴？答案是肯定的，但有一个注意点：profunctor 组合的结合律和恒等律只在自然同构意义下成立。这样一个法则只在同构意义下有效的范畴，称为双范畴（bicategory，它比 2-范畴更一般）。所以我们得到一个双范畴 Prof，其中对象是范畴，态射是 profunctor，态射之间的态射（也称 two-cells）是自然变换。
事实上，还可以更进一步，因为除了 profunctor 之外，我们还有普通函子作为范畴之间的态射。具有两种态射类型的范畴称为双重范畴（double category）。
profunctor 在 Haskell 的 lens 库和 arrow 库中扮演重要角色。