Haskell/范畴论

本文将概述 Haskell 里应用的一个概念，范畴论。因此 Haskell 代码的展示将会伴随其对应的数学定义，为了让读者可以直观地理解范畴论的概念以及它与 Haskell 的关系，这种对应可能不那么绝对的严谨。

范畴论是什么[编辑]

如图所示为一个简单的范畴，其包含三个对象，A，B，C，三个单位态射 $\operatorname {id} _{A}$ , $\operatorname {id} _{B}$ 和 $\operatorname {id} _{C}$ ，其他的两个态射 $f:C\to B$ 和 $g:A\to B$ 。图中没有展示范畴的第三个组成元素（即态射组合）。

范畴，本质上是一个简单的集合，包括三个组成元素：

对象.
态射，每个态射将两个对象（源对象和目标对象）连接在一起（它们有时被称为箭头（arrows），但本文避免使用该术语，因为它在 Haskell 中具有其他涵义。）如果 f 是源对象 A 到目标对象 B 的态射，写作 $f:A\to B$ 。
态射组合。例如：态射 $g:A\to B$ 和态射 $f:B\to C$ 可以组合为态射 $f\circ g:A\to C$ 。

许多东西都可以称为范畴。例如，所有集合构成了范畴 Set，其态射为集合间的函数，而态射组合则为一般的函数复合（标粗的为范畴名）。全部的群构成了范畴 Grp，保持群结构的函数就是它的态射（群同态），比如任意两个群 G 和 H ，G 的操作符为 * ，H 的操作符是 · ，那么函数 $f:G\to H$ 只要满足如下条件就是一个态射： $f(u*v)=f(u)\cdot f(v)$

这么看来貌似态射就是函数，但是事实并非如此。例如，任何偏序结构 (P, $\leq$ ) 都构成范畴，P 中的元素构成了该范畴的对象，任意两个元素 a 和 b 只要满足 a $\leq$ b ，那么存在态射 a \to b。另外，在相同的源对象和目的对象之间可以存在多个态射；以 Set 范畴为例， $\sin$ 和 $\cos$ 都是从源对象 $\mathbb {R}$ （实数集）到目标对象 $[-1,1]$ 的函数，但是它们是不同的态射。

范畴公理[编辑]

范畴需要符合三条定律。第一条，也是最简单的一条，态射的组合操作需要满足结合律。

f\circ (g\circ h)=(f\circ g)\circ h

态射在 Haskell 中从右到左执行，因此使用 $f\circ g$ 时，g 先执行，然后 f。

第二条，态射在组合操作下是闭合的。因此，如果存在态射 $f:B\to C$ 和 $g:A\to B$ ，那么范畴 $h=f\circ g$ 中一定会存在态射 $h:A\to C$ 。以下面范畴为例。

f 和 g 都是态射，所以我们一定能够通过组合他们在范畴中得到另一个态射。那么哪一个是态射 $f\circ g$ 呢？唯一可能的答案就是 $id_{A}$ 。同样，我们可以得到 $g\circ f=id_{B}$ 。

最后一条，在一个范畴 C 中，每一个对象 A 都会有一个单位态射， $id_{A}:A\to A$ ，这个态射是组合操作的单位元。准确的说对于每一个态射 $g:A\to B$ ：存在

g\circ \operatorname {id} _{A}=\operatorname {id} _{B}\circ g=g

请注意，涉及组合操作的表达式 $(o)$ 可以彼此相等，但各个态射不能相等。例如有两个态射从对象 A 到对象 B，即 $f:A\to B$ 和 $g:A\to B$ ，表达式 $(A\to B)$ 相同，但态射 $f=g$ 永远为假。

Hask，Haskell 范畴[编辑]

本节我们主要讨论范畴 Hask，其对象为 Haskell 中的类型，态射为 Haskell 中的函数，态射组合操作为 (·)，在 Hask 中函数 f :: A -> B 为类型 A 到 B 的态射。范畴第一第二定律很容易验证，我们知道 (·) 是一个组合操作，显然，对于任何 f 和 g ，f . g是一个新的函数。在 Hask 中，单位态射是 id，所以很容易验证第三定律：id . f = f . id = f

^[1]上面的定律并不是一个十分准确的转换，因为我们忽略了下标。在 Haskell 中函数 id 是 多态的 — 它的域和范围可以采用许多不同的类型，用范畴的概念解释就是可以存在许多不同的源对象和目标对象。但是范畴论中的态射是定义为 单态的 — 每个态射都有一个特定的源对象和一个特定的目标对象（注意：这里的单态不在范畴论上使用）。多态 Haskell 函数可以通过指定其类型（用单态类型 实例化）来实现单态，因此我们说 Hask 上类型 A 的单位态射是 (id :: A -> A) 会更精确。考虑到这一点，上述定律将被重新书写为： (id :: B -> B) . f = f . (id :: A -> A) = f 但是为简单起见，当含义明确时，我们将忽略这种区别。

练习

如上所述，任何偏序 (P, $\leq$ )都是一个范畴，其中对象为 P 的元素，任意两个元素 a 和 b 只要满足 a $\leq$ b ，那么存在态射 $a\to b$ 。问上述哪些定律保证了 $\leq$ 的传递性？
（难度增加。）如果我们在上面的例子中添加另一个态射 h，如下图所示，它就不能成为一个范畴了。为什么？提示：从态射组合方面去考虑。

函子[编辑]

A functor between two categories, $\mathbf {C}$ and $\mathbf {D}$ . Of note is that the objects A and B both get mapped to the same object in $\mathbf {D}$ , and that therefore g becomes a morphism with the same source and target object (but isn't necessarily an identity), and $\operatorname {id} _{A}$ and $\operatorname {id} _{B}$ become the same morphism. The arrows showing the mapping of objects are shown in a dotted, pale olive. The arrows showing the mapping of morphisms are shown in a dotted, pale blue.

所以我们有了一些范畴，其包含对象以及将这些对象联系在一起的态射。下一个在范畴论中非常重要的概念是functor，他们将范畴联系在了一起。functor 的实质是范畴之间的转换关系，因此对于范畴 C 和 D，有 functor $F:C\to D$ ：

映射范畴 C 中任一对象 A 到范畴 D 中的对象 $F(A)$ 。
映射范畴 C 中任一态射 $f:A\to B$ 到范畴 D 中态射 $F(f):F(A)\to F(B)$ 。

// 未翻译完

↑ Actually, there is a subtlety here: because (.) is a lazy function, if f is undefined, we have that id . f = \_ -> ⊥. Now, while this may seem equivalent to ⊥ for all intents and purposes, you can actually tell them apart using the strictifying function seq, meaning that the last category law is broken. We can define a new strict composition function, f .! g = ((.) $! f) $! g, that makes Hask a category. We proceed by using the normal (.), though, and attribute any discrepancies to the fact that seq breaks an awful lot of the nice language properties anyway.

[1] Actually, there is a subtlety here: because (.) is a lazy function, if f is undefined, we have that id . f = \_ -> ⊥. Now, while this may seem equivalent to ⊥ for all intents and purposes, you can actually tell them apart using the strictifying function seq, meaning that the last category law is broken. We can define a new strict composition function, f .! g = ((.) $! f) $! g, that makes Hask a category. We proceed by using the normal (.), though, and attribute any discrepancies to the fact that seq breaks an awful lot of the nice language properties anyway.

[1]