Haskell/範疇論

範疇論 (解決方案)

更廣泛的理論

語義學
等式推理
 程式推導
 範疇論
 Curry–Howard 同構
 fix 和遞迴

編輯此章節

本文試圖概述範疇論，因為它適用於 Haskell。為此，將在數學定義旁邊給出 Haskell 程式碼。不會完全遵循嚴格性，相反，我們希望讓讀者直觀地瞭解範疇論的概念以及它們如何與 Haskell 相關聯。

範疇簡介

一個簡單的範疇，有三個物件 A、B 和 C，三個恆等態射 $\operatorname {id} _{A}$ 、 $\operatorname {id} _{B}$ 和 $\operatorname {id} _{C}$ ，以及另外兩個態射 $f:C\to B$ 和 $g:A\to B$ 。第三個元素（態射如何組合的規範）沒有顯示。

本質上，範疇是一個簡單的集合。它有三個組成部分

物件的集合。
態射的集合，每個態射將兩個物件（源物件 和 目標物件）聯絡在一起。（這些有時被稱為箭頭，但我們在這裡避免使用該術語，因為它在 Haskell 中有其他含義。）如果 f 是一個源物件為 C，目標物件為 B 的態射，我們寫成 $f:C\to B$ .
組合這些態射的概念。如果 $g:A\to B$ 和 $f:B\to C$ 是兩個態射，它們可以被組合，得到一個態射 $f\circ g:A\to C$ .

很多東西都構成範疇。例如，Set 是所有集合的範疇，其中態射是標準函式，組合是標準函式組合。（範疇名稱通常以粗體表示。）Grp 是所有群的範疇，其中態射是保留群運算的函式（群同態），即對於任意兩個群，G 的運算為 *，H 的運算為 ·，一個函式 $k:G\to H$ 是 Grp 中的態射，如果

k(u*v)=k(u)\cdot k(v)

雖然看起來態射總是函式，但情況並非總是如此。例如，任何偏序集 (P, $\leq$ ) 定義了一個範疇，其中物件是 P 的元素，並且在任意兩個物件 A 和 B 之間存在態射當且僅當 $A\leq 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:A\to C$ ，使得 $h=f\circ g$ 。我們可以使用以下範疇來觀察它是如何工作的

f 和 g 都是態射，因此我們必須能夠將它們複合並得到範疇中的另一個態射。那麼哪個態射是 $f\circ g$ ？唯一的選擇是 $\operatorname {id} _{A}$ 。類似地，我們看到 $g\circ f=\operatorname {id} _{B}$ 。

最後，給定一個類別C，對於每個物件 $A$ ，都需要一個恆等態射， $\operatorname {id} _{A}:A\to A$ ，它是與其他態射覆合的恆等元素。準確地說，對於每個態射 $g:A\to B$

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

Hask，Haskell 類別

本文將關注的重點是Hask類別，它將 Haskell 型別視為物件，Haskell 函式視為態射，並使用(.)作為複合運算子：對於型別A和B的函式f :: A -> B是Hask中的態射。我們可以輕鬆驗證第一和第二定律：我們知道(.)是一個結合函式，並且顯然，對於任何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。上面哪條定律保證了 $\leq$ 的傳遞性？（較難）如果我們在上面示例中新增另一個態射，如下所示，它將不再是一個類別。為什麼？提示：考慮複合運算子的結合性。

函子

因此我們有一些類別，它們具有將物件關聯起來的物件和態射。類別理論中的下一個重大主題是函子，它將類別關聯起來。函子本質上是類別之間的變換，因此給定類別C和D，函子 $F:C\to D$

將C中的任何物件A對映到D中的 $F(A)$ 。
將C中的態射 $f:A\to B$ 對映到D中的 $F(f):F(A)\to F(B)$ 。

函子一個典型的例子是遺忘函子 $\mathbf {Grp} \to \mathbf {Set}$ ，它將群對映到它們的基礎集合，將群同態對映到在集合而不是群上定義的行為相同的函式。另一個例子是冪集函子 $\mathbf {Set} \to \mathbf {Set}$ ，它將集合對映到它們的冪集，並將函式 $f:X\to Y$ 對映到函式 ${\mathcal {P}}(X)\to {\mathcal {P}}(Y)$ ，它以輸入 $U\subseteq X$ 並返回 $f(U)$ ，即U在f下的像，定義為 $f(U)=\{\,f(u):u\in U\,\}$ 。對於任何範疇C，我們可以定義一個稱為C上的恆等函子的函子，或 $1_{C}:C\to C$ ，它只是將物件對映到它們自身，將態射對映到它們自身。這將在後面的單子定律部分中被證明是有用的。

再次強調，函子必須服從一些公理。首先，給定物件A上的恆等態射 $\operatorname {id} _{A}$ ， $F(\operatorname {id} _{A})$ 必須是 $F(A)$ 上的恆等態射，即

F(\operatorname {id} _{A})=\operatorname {id} _{F(A)}

其次，函子必須在態射覆合上分配，即

F(f\circ g)=F(f)\circ F(g)

練習
對於右邊給出的圖表，檢查這些函子定律。

Hask上的函子

您可能在 Haskell 中見過的 Functor 型別類實際上與函子的範疇論概念相關。請記住，函子有兩個部分：它將一個範疇中的物件對映到另一個範疇中的物件，並將第一個範疇中的態射對映到第二個範疇中的態射。Haskell 中的函子是從 Hask 到 func 的，其中 func 是 Hask 的一個子範疇，僅定義在該函子的型別上。例如，列表函子是從 Hask 到 Lst 的，其中 Lst 是僅包含 列表型別 的範疇，即任何型別 T 的 [T]。Lst 中的態射是在列表型別上定義的函式，即對於型別 T、U 的函式 [T] -> [U]。這如何與 Haskell 型別類 Functor 聯絡起來呢？回顧其定義

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b

讓我們舉一個示例例項，

instance Functor Maybe where
  fmap f (Just x) = Just (f x)
  fmap _ Nothing  = Nothing

關鍵部分在於：型別構造器 Maybe 將任何型別 T 轉換為一個新型別 Maybe T。此外，fmap 限制在 Maybe 型別上，它將函式 a -> b 轉換為函式 Maybe a -> Maybe b。但僅此而已！我們定義了兩個部分，一個將 Hask 中的物件對映到另一個範疇中的物件（即 Maybe 型別和在 Maybe 型別上定義的函式），另一個將 Hask 中的態射對映到該範疇中的態射。因此，Maybe 是一個函子。

關於 Haskell 函子的一個有用的直覺是它們代表可以對映的型別。這可以是列表或 Maybe，也可以是樹等更復雜結構。使用 fmap 可以編寫執行某些對映的函式，然後可以將任何函子結構傳遞到該函式中。例如，您可以編寫一個通用的函式，它涵蓋所有 Data.List.map、Data.Map.map、Data.Array.IArray.amap 等等。

函子公理呢？多型函式 id 代替了任何 A 的 $\operatorname {id} _{A}$ ，因此第一個定律指出

fmap id = id

考慮到我們上面的直覺，這說明對一個結構進行對映，而對每個元素都不做任何操作，等同於不做任何操作。其次，態射覆合就是 (.)，所以

fmap (f . g) = fmap f . fmap g

這個第二個定律在實踐中非常有用。將函子想象成列表或類似的容器，右側是一個兩遍演算法：我們對結構進行對映，執行 g，然後再次對其進行對映，執行 f。函子公理保證我們可以將其轉換為一個執行 f . g 的單遍演算法。這是一個稱為融合的過程。

練習
檢查 Maybe 和列表函子的定律。

將範疇論概念轉換為 Haskell

函子提供了一個很好的例子，說明範疇論是如何被轉換為 Haskell 的。需要記住的關鍵點是

我們在 Hask 及其子範疇中工作。
物件是型別。
態射是函式。
接受一個型別並返回另一個型別的函式是型別構造器。
接受一個函式並返回另一個函式的函式是高階函式。
型別類及其提供的多型性，為捕捉範疇論中事物通常在多個物件上定義這一事實提供了一種很好的方式。

單子

單子顯然是 Haskell 中一個極其重要的概念，事實上它們最初來自範疇論。單子是一種特殊的函子，從一個範疇到同一個範疇，它支援一些額外的結構。因此，讓我們從定義開始。單子是一個函子 $M:C\to C$ ，以及對於 C 中的每個物件 X，有兩個態射^[2]

$\operatorname {unit} _{X}^{M}:X\to M(X)$
$\operatorname {join} _{X}^{M}:M(M(X))\to M(X)$

當所討論的單子很明顯時，我們會省略這些函式的 M 上標，只討論一些 X 的 $\operatorname {unit} _{X}$ 和 $\operatorname {join} _{X}$ 。

那麼，讓我們看看這如何轉換為 Haskell 型別類 Monad。

class Functor m => Monad m where
  return :: a -> m a
  (>>=)  :: m a -> (a -> m b) -> m b

Functor m 的類約束確保我們已經有了函子結構：物件和態射的對映。return 是任何 X 的 $\operatorname {unit} _{X}$ 的（多型）類似物。但是我們遇到了一個問題。儘管 return 的型別看起來與 unit 的型別非常相似；另一個函式 (>>=)，通常稱為 bind，與 join 沒有任何相似之處。然而，另一個單子函式 join :: Monad m => m (m a) -> m a，看起來很相似。事實上，我們可以從彼此中恢復 join 和 (>>=)

join :: Monad m => m (m a) -> m a
join x = x >>= id

(>>=) :: Monad m => m a -> (a -> m b) -> m b
x >>= f = join (fmap f x)

因此，指定一個單子的 `return`、`fmap` 和 `join` 等同於指定它的 `return` 和 `(>>=)`. 事實上，在範疇論中定義單子的正常方式是給出 *unit* 和 *join*，而 Haskell 程式設計師更喜歡給出 `return` 和 `(>>=)`.^[3] 很多時候，範疇論的方式更有意義。只要你擁有某種結構 * $M$ 以及將任何物件 * $X$ 轉化為 $M(X)$ 的自然方式，以及將 $M(M(X))$ 轉化為 $M(X)$ 的方式，你很可能就擁有一個單子。在接下來的示例部分中，我們可以看到這一點。

示例：冪集函子也是一個單子

上面描述的冪集函子 $P:\mathbf {Set} \to \mathbf {Set}$ 構成了一個單子。對於任何集合 *S*，你都有一個 $\operatorname {unit} _{S}(x)=\{x\}$ ，它將元素對映到它們的單元素集合。請注意，這些單元素集合都是 *S* 的平凡子集，因此 $\operatorname {unit} _{S}$ 返回 *S* 的冪集中的元素，這是必需的。此外，你可以定義一個函式 $\operatorname {join} _{S}$ ，如下所示：我們接收一個輸入 $L\in {\mathcal {P}}({\mathcal {P}}(S))$ 。這是

*S* 的冪集的冪集的成員。
因此是 *S* 的所有子集的集合的所有子集的集合的成員。
因此是 *S* 的子集的集合

然後我們返回這些子集的並集，得到 *S* 的另一個子集。符號上，

\operatorname {join} _{S}(L)=\bigcup L

.

因此 *P* 是一個單子^[4].

事實上，*P* 幾乎等同於列表單子；除了我們談論的是列表而不是集合，它們幾乎是一樣的。請比較

Set 上的冪集函子
函式型別	定義
給定一個集合 S 和一個態射 $f:A\to B$
$P(f):{\mathcal {P}}(A)\to {\mathcal {P}}(B)$	$(P(f))(S)=\{f(a):a\in S\}$
$\operatorname {unit} _{S}:S\to {\mathcal {P}}(S)$	$\operatorname {unit} _{S}(x)=\{x\}$
$\operatorname {join} _{S}:{\mathcal {P}}({\mathcal {P}}(S))\to {\mathcal {P}}(S)$	$\operatorname {join} _{S}(L)=\bigcup L$
Haskell 中的列表單子
函式型別	定義
給定型別 `T` 和函式 `f :: A -> B`
`fmap f :: [A] -> [B]`	`fmap f xs = [ f a \| a <- xs ]`
`return :: T -> [T]`	`return x = [x]`
`join :: [[T]] -> [T]`	`join xs = concat xs`

單子定律及其重要性

就像函子為了被稱為函子必須遵守某些公理一樣，單子也有一些自己的公理。我們首先列出它們，然後翻譯成 Haskell，最後看看它們為什麼如此重要。

給定一個單子 $M:C\to C$ 和一個態射 $f:A\to B$ 對於 $A,B\in C$ ,

$\mathrm {join} \circ M(\mathrm {join} )=\mathrm {join} \circ \mathrm {join}$
$\mathrm {join} \circ M(\mathrm {unit} )=\mathrm {join} \circ \mathrm {unit} =\mathrm {id}$
$\mathrm {unit} \circ f=M(f)\circ \mathrm {unit}$
$\mathrm {join} \circ M(M(f))=M(f)\circ \mathrm {join}$

現在，Haskell 翻譯應該不言自明瞭

join . fmap join = join . join
join . fmap return = join . return = id
return . f = fmap f . return
join . fmap (fmap f) = fmap f . join

(記住 fmap 是函子的作用於態射的部分。) 這些定律乍一看有點難以理解。這些定律到底意味著什麼，為什麼它們應該對單子成立？讓我們來探索一下這些定律。

第一定律

join . fmap join = join . join

為了理解這個定律，我們首先以列表為例。第一定律提到了兩個函式，join . fmap join（左側）和 join . join（右側）。這些函式的型別會是什麼？記住 join 的型別是 [[a]] -> [a]（我們現在只談論列表），所以這兩個型別的型別都是 [[[a]]] -> [a]（它們相同的事實很有用；畢竟，我們試圖證明它們完全相同函式！）。所以我們有一個列表的列表的列表。然後，左側對這個三層列表執行 fmap join，然後對結果使用 join。fmap 只是列表中熟悉的 map，所以我們首先對頂層列表中每個列表的列表進行對映，將它們連線成一個列表。因此，之後我們有一個列表的列表，然後我們將其執行到 join 中。總而言之，我們“進入”頂層，將第二層和第三層摺疊起來，然後將這個新層與頂層摺疊起來。

右側呢？我們首先對我們的列表的列表的列表執行 join。儘管這是三層，而你通常將一個兩層列表應用於 join，但這仍然會起作用，因為 [[[a]]] 只是 [[b]]，其中 b = [a]，所以從某種意義上說，一個三層列表只是一個兩層列表，但最後一層不是“扁平”的，而是由另一個列表組成。因此，如果我們將我們的列表的列表（的列表）應用於 join，它將把最外層的兩層扁平化成一層。由於第二層不是扁平的，而是包含第三層，因此我們最終仍然會得到一個列表的列表，另一個 join 會將其扁平化。總結一下，左側將把內層的兩層扁平化成一個新層，然後將這個層與最外層扁平化。右側將首先扁平化外層的兩層，然後將這個層與最內層扁平化。這兩個操作應該是等效的。這有點像 join 的結合律。

Maybe 也是一個單子，有

return :: a -> Maybe a
return x = Just x

join :: Maybe (Maybe a) -> Maybe a
join Nothing         = Nothing
join (Just Nothing)  = Nothing
join (Just (Just x)) = Just x

因此，如果我們有一個三層的 Maybe（即，它可能是 Nothing，Just Nothing，Just (Just Nothing) 或者 Just (Just (Just x))），第一定律表示先摺疊內層的兩層，然後與外層摺疊完全等效於先摺疊外層，然後與最內層摺疊。

練習
使用一些示例驗證列表和 Maybe 單子是否確實遵循此定律，以準確瞭解層級扁平化的工作原理。

第二定律

join . fmap return = join . return = id

那麼第二定律呢？同樣，我們將從列表的例子開始。第二定律中提到的兩個函式都是 [a] -> [a] 型別的函式。左側表示一個函式，它遍歷列表，將每個元素 x 轉換為其單例列表 [x]，這樣最終我們就剩下一個單例列表的列表。這個兩層列表使用 join 再次扁平化為單層列表。然而，右側則將整個列表 [x, y, z, ...] 轉換為列表的單例列表 [[x, y, z, ...]]，然後將兩層再次扁平化為一層。這條定律不太容易快速說明，但它本質上說的是，將 return 應用於單子值，然後 join 結果，無論是在頂層內部還是外部執行 return，都應該具有相同的效果。

練習
證明 Maybe 單子的這條第二定律。

第三和第四定律

return . f = fmap f . return

join . fmap (fmap f) = fmap f . join

最後兩條定律表達了我們對單子的期望行為的更直觀的事實。最簡單的理解其真偽的方法是將其擴充套件為使用擴充套件形式

\x -> return (f x) = \x -> fmap f (return x)
\x -> join (fmap (fmap f) x) = \x -> fmap f (join x)

練習
透過探索它們的含義，以類似於我們解釋第一和第二定律的方式，說服自己這些定律應該適用於任何單子。

對 do 塊的應用

嗯，我們對單子必須支援的定律有了直觀的描述，但這為什麼很重要呢？當我們考慮 do 塊時，答案就變得顯而易見了。回想一下，do 塊只是涉及 (>>=) 的語句組合的語法糖，正如通常的翻譯所證明的那樣

do { x }                 -->  x
do { let { y = v }; x }  -->  let y = v in do { x }
do { v <- y; x }         -->  y >>= \v -> do { x }
do { y; x }              -->  y >>= \_ -> do { x }

還要注意，我們可以使用我們上面定律中的 return 和 (>>=) 來證明通常被引用為單子定律的東西（證明在某些情況下有點繁瑣，如果你想跳過它們，請隨意跳過）

return x >>= f = f x。證明

   return x >>= f
 = join (fmap f (return x)) -- By the definition of (>>=)
 = join (return (f x))      -- By law 3
 = (join . return) (f x)
 = id (f x)                 -- By law 2
 = f x

m >>= return = m。證明

   m >>= return
 = join (fmap return m)    -- By the definition of (>>=)
 = (join . fmap return) m
 = id m                    -- By law 2
 = m

(m >>= f) >>= g = m >>= (\x -> f x >>= g)。證明（回想一下 fmap f . fmap g = fmap (f . g)）

   (m >>= f) >>= g
 = (join (fmap f m)) >>= g                          -- By the definition of (>>=)
 = join (fmap g (join (fmap f m)))                  -- By the definition of (>>=)
 = (join . fmap g) (join (fmap f m))
 = (join . fmap g . join) (fmap f m)
 = (join . join . fmap (fmap g)) (fmap f m)         -- By law 4
 = (join . join . fmap (fmap g) . fmap f) m
 = (join . join . fmap (fmap g . f)) m              -- By the distributive law of functors
 = (join . join . fmap (\x -> fmap g (f x))) m
 = (join . fmap join . fmap (\x -> fmap g (f x))) m -- By law 1
 = (join . fmap (join . (\x -> fmap g (f x)))) m    -- By the distributive law of functors
 = (join . fmap (\x -> join (fmap g (f x)))) m
 = (join . fmap (\x -> f x >>= g)) m                -- By the definition of (>>=)
 = join (fmap (\x -> f x >>= g) m)
 = m >>= (\x -> f x >>= g)                          -- By the definition of (>>=)

這些使用 return 和 (>>=) 的新單子定律可以翻譯成 do 塊表示法。

無點風格	do 塊風格
`return x >>= f = f x`	`do { v <- return x; f v } = do { f x }`
`m >>= return = m`	`do { v <- m; return v } = do { m }`
`(m >>= f) >>= g = m >>= (\x -> f x >>= g)`	do { y <- do { x <- m; f x }; g y } = do { x <- m; y <- f x; g y }

現在，單子定律就變成了關於 do 塊應該如何工作的常識性陳述。如果其中一條定律失效，使用者就會感到困惑，因為你將無法像預期的那樣在 do 塊中進行操作。本質上，單子定律是可用性指南。

練習

事實上，我們給出的兩種定律版本

-- Categorical:
join . fmap join = join . join
join . fmap return = join . return = id
return . f = fmap f . return
join . fmap (fmap f) = fmap f . join

-- Functional:
m >>= return = m
return m >>= f = f m
(m >>= f) >>= g = m >>= (\x -> f x >>= g)

完全等價。我們已經證明可以從範疇定律中恢復函式定律。反過來，從函式定律出發，證明範疇定律成立。記住以下定義可能會有所幫助

join m = m >>= id
fmap f m = m >>= return . f

感謝 Yitzchak Gale 提供了這項練習建議。

總結

在本章中，我們已經走得很遠。我們已經瞭解了什麼是範疇，以及它們如何應用於 Haskell。我們介紹了範疇論的基本概念，包括函子，以及一些更高階的主題，比如單子，並看到了它們對 Haskell 慣用語法的關鍵作用。我們沒有涵蓋一些對我們的目標來說不必要的範疇論基礎知識，比如自然變換，而是為 Haskell 結構背後的範疇基礎提供了直觀的感受。

備註

↑ 實際上，這裡有一個細微之處：因為 (.) 是一個惰性函式，如果 f 是 undefined，我們就有 id . f = \_ -> ⊥。現在，雖然這在所有意圖和目的上似乎等同於 ⊥，但實際上你可以使用嚴格化函式 seq 將它們區分開來，這意味著最後一條範疇定律被破壞了。我們可以定義一個新的嚴格組合函式 f .! g = ((.) $! f) $! g，它使 Hask 成為一個範疇。然而，我們將繼續使用正常的 (.)，並將任何差異歸因於 seq 實際上破壞了很多很好的語言屬性這一事實。
↑ 經驗豐富的範疇論者會注意到我們在這裡簡化了一些東西；與其將單位和連線作為自然變換，不如將它們的自然性作為額外公理（定律 3 和 4）與標準單子定律（定律 1 和 2）一起新增。理由是簡單；我們不是要教授整個範疇論，只是為 Haskell 中的一些結構提供範疇背景。你可能還會注意到，我們給這些態射起了類似於它們的 Haskell 類似物的名稱，因為名稱 $\eta$ 和 $\mu$ 並沒有提供太多的直覺。
↑ 這可能是由於 Haskell 程式設計師喜歡將單子視為一種具有共同特徵的順序執行計算的方法，而在範疇論中，各種結構的容器方面更為突出。join 自然地適用於容器（將容器的兩個層級壓縮為一個），而 (>>=) 是自然的順序執行操作（執行某項操作，將結果饋送到其他操作中）。
↑ 如果你能證明某些定律成立，我們將在下一節中探討。