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]