Haskell/範疇論

維基教科書,自由的教學讀本
跳至導覽 跳至搜尋

本文將概述 Haskell 里應用的一個概念,範疇論。因此 Haskell 代碼的展示將會伴隨其對應的數學定義,為了讓讀者可以直觀地理解範疇論的概念以及它與 Haskell 的關係,這種對應可能不那麼絕對的嚴謹。

範疇論是什麼[編輯]

如圖所示為一個簡單的範疇,其包含三個對象,ABC, 三個單位態射 , ,其他的兩個態射 。圖中沒有展示範疇的第三個組成元素(即態射組合)。

範疇,本質上是一個簡單的集合,包括三個組成元素:

  • 對象.
  • 態射,每個態射將兩個對象(源對象和目標對象)連接在一起(它們有時被稱為箭頭(arrows),但本文避免使用該術語,因為它在 Haskell 中具有其他涵義。)如果 f 是源對象 A 到目標對象 B 的態射,寫作
  • 態射組合。例如:態射 和 態射 可以組合為態射

許多東西都可以稱為範疇。例如,所有集合構成了範疇 Set,其態射為集合間的函數,而態射組合則為一般的函數複合(標粗的為範疇名)。全部的群構成了範疇 Grp,保持群結構的函數就是它的態射(群同態),比如任意兩個群 GH ,G 的操作符為 *H 的操作符是 · ,那麼函數 只要滿足如下條件就是一個態射:






這麼看來貌似態射就是函數,但是事實並非如此。例如,任何偏序結構 (P, ) 都構成範疇,P 中的元素構成了該範疇的對象,任意兩個元素 ab 只要滿足 a b ,那麼存在態射 a \to b。另外,在相同的源對象和目的對象之間可以存在多個態射;以 Set 範疇為例, 都是從源對象 (實數集) 到目標對象 的函數,但是它們是不同的態射。

範疇公理[編輯]

範疇需要符合三條定律。第一條,也是最簡單的一條,態射的組合操作需要滿足結合律

態射在 Haskell 中從右到左執行,因此使用時,g 先執行,然後 f

第二條,態射在組合操作下是閉合的。因此,如果存在態射 ,那麼範疇 中一定會存在態射 。以下面範疇為例。

Composition-ex.png

fg 都是態射,所以我們一定能夠通過組合他們在範疇中得到另一個態射。 那麼哪一個是態射 呢?唯一可能的答案就是 。同樣,我們可以得到

最後一條,在一個範疇 C 中,每一個對象 A 都會有一個單位態射,這個態射是組合操作的單位元。準確的說對於每一個態射 :存在

請注意,涉及組合操作的表達式可以彼此相等,但各個態射不能相等。例如有兩個態射從對象 A 到對象 B,即 ,表達式 相同,但態射 永遠為假。

Hask,Haskell 範疇[編輯]

本節我們主要討論範疇 Hask,其對象為 Haskell 中的類型,態射為 Haskell 中的函數,態射組合操作為 (·),在 Hask 中函數 f :: A -> B 為類型 AB 的態射。範疇第一第二定律很容易驗證,我們知道 (·) 是一個組合操作,顯然,對於任何 fgf . 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, )都是一個範疇,其中對象為 P 的元素,任意兩個元素 ab 只要滿足 a b ,那麼存在態射 。問上述哪些定律保證了 的傳遞性?
  • (難度增加。)如果我們在上面的例子中添加另一個態射 h,如下圖所示,它就不能成為一個範疇了。為什麼?提示:從態射組合方面去考慮。
Not-a-cat.png

函子[編輯]

A functor between two categories, and . Of note is that the objects A and B both get mapped to the same object in , and that therefore g becomes a morphism with the same source and target object (but isn't necessarily an identity), and and 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 的實質是範疇之間的轉換關係,因此對於範疇 CD,有 functor

  • 映射範疇 C 中任一對象 A 到範疇 D 中的對象
  • 映射範疇 C 中任一態射 到範疇 D 中態射

// 未翻譯完

  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.