<譯> 天然變換

原文:https://bartoszmilewski.com/2...c++

上一篇:函數類型程序員

譯註:因爲距離以前的翻譯的時間過久,因此有些內容可能有點不太相符。待我找時間校對。編程

咱們已經討論過,函子能夠在維持範疇結構的前提下實現範疇之間的映射。函子能夠將一個範疇嵌入到另外一個範疇,它也可讓多個範疇坍縮爲一個範疇且不會破壞範疇的結構。憑藉函子,咱們能夠在一個範疇以內構建另外一個範疇。源範疇可視爲目標範疇的部分結構的模型或藍圖。segmentfault

範疇的嵌入

將一個範疇嵌入到另外一個範疇可能有許多種方式。有時這些方式是等價的,有時它們不等價。你能夠將整個的範疇坍縮爲另外一個範疇中的一個對象,也能夠將一個範疇中的每一個對象映射爲另外一個範疇中不一樣的對象,將前者中的每一個態射映射爲後者中的不一樣的態射。一樣的想法能夠有多種不一樣方式的實現。天然變換能夠幫助咱們對比這些實現。天然變換是函子之間的映射——能夠保持函子性質不變的特殊映射。函數

對於範疇 CD 之間的兩個函子 FG,若是咱們只關注 C 中的一個對象 a,它被映射爲 D 中的兩個對象:F aG a,那麼應該存在一個函子映射,它能夠將 F a 映射爲 G a測試

函子映射

因爲在同一範疇中的對象映射應該不會脫離該範疇,並且咱們不想人工創建 F aG a 的聯繫,所以很天然的考慮使用既有的聯繫——所謂的態射。天然變換本質上是如何選取態射:對於任意對象 $a$,天然變換就是選取一個從 F aG a 的態射。若是將一個天然變換稱爲 α,那麼這個態射就被稱爲在 a 上的 α 份量(Component of α at a),記做 α_a優化

α_a :: F a -> G a

譯註: α_a 表示 $\alpha_a$。用 HTML 標記來表示,就是 α<sub>a</sub>。因爲許多號稱支持 Markdown 文檔格式的網站,它們不支持在 Markdown 裏自由使用 HTML 標記。雖然這些網站有一些也支持 TeX 公式,可是又無法在代碼排版環境中嵌入 TeX 公式。所以,我不得不使用下劃線來表示公式裏的下標。在下文,我也會使用 ^ 來表示上標,順便說一句,我對如今幾乎任何一個由用戶自行發佈內容的網站都不滿意。網站

記住,a 是一個在 C 中的對象,而 α_aD 中的一個態射。spa

對於某個 a,若是在 F aG a 之間沒有態射,那麼 FG 之間也就不存在天然變換。翻譯

故事剛剛說了一半。函子所映射的不止是對象,它們也能映射態射,天然變換應該如何對待這種映射?答案是,態射的映射是固定的——在 FG 之間的任何一個天然變換下,F f 必須變換成 G f。也就是說,兩個函子對態射所造成的映射會完全限制與之相適的天然變換的定義。來考慮在範疇 C 中的兩個對象 ab 之間的態射 f,它被映射爲範疇 D 中的兩個態射 F fG f

F f :: F a -> F b
G f :: G a -> G b

天然變換 α 提供兩個附加的態射來補全 D 中的結構:

α_a :: F a -> G a
α_b :: F b -> G b

D 中的結構

如今,咱們便有了兩個從 F aG b 的途徑。爲了保證這兩種途徑等價,必須引入天然性條件(Naturality condition):

G f ∘ α_a = α_b ∘ F f

這個條件應該對於任意的 f 都成立。

天然性條件很是有用。例如,若是態射 F f 是可逆的,天然性決定了以 α_a 形式表示的 α_b。經過 f,基於天然性條件可將 α_a 變換爲:

α_b = (G f) ∘ α_a ∘ (F f)^(-1)>

天然性條件的做用

若是兩個對象之間存在多個可逆的態射,上述變換也都成立。儘管態射一般是不可逆的,可是我想說的是兩個函子之間的天然變換並不是必定存在。所以,與天然變換相關的函子的多寡,可在很大程度上顯現這些函子所操縱的範疇的結構。在講極限與 Yoneda 定理時,我會給出一些例子。

從份量的角度來看天然變換,您能夠認爲它將對象映射爲態射。可是,從天然性條件的角度來看,你也能夠認爲它將態射映射爲四方形的交換圖(Commuting squares)—— C 中的每一個態射都被映射爲 D 中的一個交換圖。

天然性

天然變換的這一性質可讓不少範疇便於構造,這些範疇每每包含着這類的交換圖。在正確選擇函子的狀況下,大量的交換條件都可以轉換爲天然性條件。之後在講到極限、上極限(Colimit)以及伴隨(Adjunction)時會給出一些例子。

最後,天然變換可用於定義函子的同構。若是說兩個函子是天然同構的,差很少是在是說它們是相同的函子。天然同構是以天然變換的形式定義的,這種天然變換的各個份量都是同構的(可逆的態射)。

多態函數

以前講過函子(更確切的說,是自函子)在編程中所扮演的角色。它們至關於類型構造子——將類型映射爲類型。不過,函子也能將函數映射爲函數,這種映射是經過一個高階函數 fmap(在 C++ 中則是 transform, then 之類的行爲)。

爲了構造一個天然變換,咱們從一個對象開始,也就是一種類型,設爲 a。一個函子 F,能夠將 a 映射爲類型 F a。另外一個函子 G,能夠將 a 映射爲 G a。在 a 上的天然變換 alpha 的份量是一個從 F aG a 的函數。使用用僞 Haskell 代碼,可將其表示爲:

alpha_a :: F a -> G a

天然變換是面向各類類型 a 的多態函數:

alpha :: forall a . F a -> G a

forall a 在 Haskell 中是可選的(能夠用語言擴展 ExplicitForAll 開啓它)。一般,可將其寫爲:

alpha :: F a -> G a

請記住,這是由 a 參數化的一個函數族。這是 Haskell 語法簡潔性的又一個示例。在 C++ 中,與之相似的構造要麻煩一些:

template<Class A> G<A> alpha(F<A>);

Haskell 的多態函數與 C++ 的泛型函數之間存在很大的區別,主要體現爲函數的實現方式以及類型檢查方式上。在 Haskell 中,一個多態函數必須對於全部類型是惟一的。一個公式必須適用於全部的類型。這就是所謂的參數化多態(Parametric polymorphism)。

C++ 默認提供的是特設多態(Ad hoc polymorphism),這意味着模板不必定涵蓋全部類型。一份模板是否適用於某種給定的類型須要在實例化時方能肯定,彼時,編譯器會用一種具體的類型來替換模板的類型參數。類型檢測是以推導的形式實現的,編譯器常常會給出難以理解的錯誤信息。

在 C++ 中,還有一種函數重載與模板特化機制,經過這種機制能夠爲不一樣的類型定義函數的不一樣版本。Haskell 也有相似的機制,即類型類(Type class)與類型族(Type family)。

Haskell 的參數化多態有一個一個不可預料的結果。凡是像這種類型的多態函數:

alpha :: F a -> G a

函子 FG 自動知足天然性條件。這裏,咱們再回到範疇論的概念(f 是一個函數,f::a->b):

G f ∘ α_a = α_b ∘ F f

在 Haskell 中,函子 G 做用於一個態射 f 是經過 fmap 實現的。可以使用 Haskell 僞碼將上述概念表示爲:

fmap_G f . alphaa = alphab . fmap_F f

歸功於 Haskell 的類型推導,上述類型標記是不須要的,所以可寫爲如下形式:

fmap f . alpha = alpha . fmap f

這依然不是真正的 Haskell 代碼——在代碼中沒法表示函數等式——不過,上式是恆等的,程序員在等式推導中可使用這個公式,此外,編譯器也能夠利用這個公式對代碼進行優化。

天然性條件之因此在 Haskell 裏會自動被知足,這是『免費的定理』的天然結果。在 Haskell 裏,參數化多態,將其用於定義天然變換,會引入很是強的限制條件——一個公式適應全部類型。這些限制條件會變成面向這些函數的方程同樣的定理。對於可以對函子進行變換的函數,免費的定理是天然性條件。(做者注:你能夠閱讀我寫的另外一篇文章《Parametricity: Money for Nothing and Theorems for Free》,會讓你對這些免費的定理可以瞭解得更多一些。)

以前我提到過,在 Haskell 裏,能夠將函子視爲泛型容器。咱們能夠繼續這個類比,將天然變換視爲一種重組方法,即將一個容器裏的東西取出來放到另外一個容器裏。咱們不會觸碰這些東西:不修改,也不創造。咱們只是將它們(或它們的一部分)複製到新的容器裏,在這個過程當中有時候會對它們做幾回乘法。

因而,天然性條件就是,首先它不關心咱們是先經過 fmap 修改這些東西,而後再將它們放到新容器裏,仍是先把它們放到新容器裏再用適用於這個容器的 fmap 去修改它們。重組與 fmap,它們是正交的,『你走你的陽關道,我過個人獨木橋』。

來看一下 Haskell 裏的天然變換。首先來看列表與 Maybe 這兩種函子之間的天然變換,它的功能是,當且僅當列表非空時返回列表的首元素:

safeHead :: [a] -> Maybe a
safeHead [] = Nothing
safeHead (x:xs) = Just x

它是面向 a 的函數多態化。它能夠不受限制地做用於任意一種類型 a,所以它是一個參數化多態的例子。從而,它就是兩個函子之間的一個天然變換。不過,如今這只是咱們在自覺得是,下面來驗證它是否符合天然性條件。

fmap f . safeHead = safeHead . fmap f

咱們要考慮兩種狀況;一個空列表:

fmap f (safeHead []) = fmap f Nothing = Nothing

safeHead (fmap f []) = safeHead [] = Nothing

和一個非空列表:

fmap f (safeHead (x:xs)) = fmap f (Just x) = Just (f x)

safeHead (fmap f (x:xs)) = safeHead (f x : fmap f xs) = Just (f x)

上面我動用了面向列表的 fmap

fmap f [] = []
fmap f (x:xs) = f x : fmap f xs

與面向 Maybefmap

fmap f Nothing = Nothing
fmap f (Just x) = Just (f x)

當函子之一是微不足道的 Const 函子的時候,會發生一件有趣的事。一個以 Const 函子爲始點或終點的天然變換,看上去就像一個函數,它即面向它的返回類型多態,也面向它的參數類型多態。

例如,可將 length 視爲從列表函子到 Const Int 函子的天然變換:

length :: [a] -> Const Int a
length [] = Const 0
length (x:xs) = Const (1 + unConst (length xs))

這裏,unConst 用於剝除 Const 構造子:

unConst :: Const c a -> c
unConst (Const x) = x

固然了,實際上 length 的定義是下面這樣:

length :: [a] -> Int

這個定義有效地掩蓋了 length 做爲天然變換的本質。

尋找一個以 Const 函子爲始點的參數化多態函數有點難,由於這須要無中生有創造一個值出來。咱們所能想到的最好的辦法是:

scam :: Const Int a -> Maybe a
scam (Const x) = Nothing

還有一個不一樣尋常的函子,咱們以前已經見過它了,它在 Yoneda 引理中扮演了重要的角色。這個函子就是 Reader 函子。下面我用 newtype 來重寫一下它的定義:

newtype Reader e a = Reader (e -> a)

這個函子被兩種類型參數化了,可是它的(逆變)函子性僅着落在第二個類型上:

instance Functor (Reader e) where  
    fmap f (Reader g) = Reader (\x -> f (g x))

對於每種類型 e,均可以定義從 Reader e 到任何其餘函子的天然變換家族。之後會看到,這個家族的成員老是與 f e 的元素壹壹對應(Yoneda 引理)。

例如,考慮有時會被忽略的僅有一個值 () 的 unit 類型 ()。函子 Reader () 接受任何一種類型 a,將它射入函數類型 () -> a。這些函數能夠從集合 a 中拮取一個元素。這些函數的數量與 a 中元素的數量同樣多。如今,來看一下從這種函子到 Maybe 函子的天然變換:

alpha :: Reader () a -> Maybe a

這樣的天然變換隻有 dumb

dumb (Reader _) = Nothing

obvious

obvious (Reader g) = Just (g ())

(用 g 能作的事情僅僅是讓它做用於 ()。)

還有,實際上按照 Yoneda 引理的說法,這些與 Maybe () 類型的兩個元素相符,即 NothingJust ()。呆會兒咱們就會再回到 Yoneda 引理上來——以上的說法有些不嚴肅。

超天然性

兩個函子之間的參數化多態函數(包括 Const 函子這種邊界狀況)一定是天然變換。由於全部的標準代數數據類型都是函子,在這些類型之間的任何一個多態函數都是天然變換。

咱們還掌握了函數類型,它們對於它們的返回類型而言具備着函子性。咱們可使用它們來構造函子(例如 Reader 函子),併爲這些函子構造天然變換——更高階的函數。

不過,對於參數類型而言,函數類型不具有協變性,它們具有逆變性。固然,逆變函子就是相反範疇中的協變函子。在範疇意義上,兩個逆變函子之間的多態函數依然可視爲天然變換,除了它們只能做用於 Haskell 類型所構成的兩個相反的範疇裏的函子。

你可能還記得以前咱們見過的一個逆變函子的示例:

newtype Op r a = Op (a -> r)

這個函子對於 a 而言具備逆變性:

instance Contravariant (Op r) where
    contramap f (Op g) = Op (g . f)

咱們能夠寫一個函數,假設它從 Op BoolOp String

predToStr (Op f) = Op (\x -> if f x then "T" else "F")

因爲這兩個函子不具有協變性,它並不是 Hask 範疇中的天然變換。不過,因爲它們都具有逆變性,因此它們知足『相反的』天然性條件:

contramap f . predToStr = predToStr . contramap f

注意,函數 f 必須得走與 fmap 的做用下的方向相反的方向,由於 contramap 的簽名是:

contramap :: (b -> a) -> (Op Bool a -> Op Bool b)

存在不是函子的類型構造子嗎,它是協變的仍是逆變的?看下面的例子:

a -> a

這不是一個函子,由於同一類型的 a 出如今負(逆變)位與正(協變)位上。對於這種類型,fmapcontramap 都沒法實現。所以,函數簽名:

(a -> a) -> f a

其中 f 是任意函子,這個函數不是天然變換。有趣的是,存在着一種廣義的天然變換,叫做雙天然變換,它們可以處理這些狀況。在咱們討論端(End)的時候會遇到它們。

函子範疇

如今,咱們有了函子之間的映射——天然變換——所以很天然地就會想到,函子是否可以造成範疇?沒錯,它們能夠。對於每對範疇而言,僅存在一個函子範疇。在這個範疇裏,對象是從 C 到 D 的函子,而態射就是這些函子之間的天然變換。

咱們必須得定義兩個天然變換的複合,不過,這至關容易。天然變換的份量是態射,而咱們知道怎樣實現態射的複合。

沒錯,咱們以從函子 F 到函子 G 的天然變換 α 爲例。它在對象 a 上的份量是某個態射:

α_a :: F a -> G a

咱們打算用對 αβ 進行復合,後者是從 GH 的天然變換。βa 上的份量是一個態射:

β_a :: G a -> H a

這些態射是可複合的,複合結果又是一個態射:

β_a ∘ α_a :: F a -> H a

能夠用這個態射做爲天然變換 $β\cdot α$ 的份量——天然變換 βa 以後的複合:

(β ⋅ α)_a = β_a ∘ α_a

天然變換的複合

仔細觀察上面這幅圖,能夠確信這種複合的結果是從 FH 的天然變換:

H f ∘ (β ⋅ α)_a = (β ⋅ α)_b ∘ F f

天然變換複合的全貌

天然變換的複合遵循結合律,由於它們的份量都是常規態射,然後者的複合是遵循結合律的。

最後,對於每一個函子 F,存在一個恆等天然變換 1_F,它的份量是恆等態射:

id_{F a} :: F a -> F a

因此,函子的確能造成範疇。

說一說記法。與 Saunders Mac Lane 同樣,上面我使用小圓點(dot)來表示各類天然變換的複合。問題是存在兩種天然變換的複合方式。一種叫豎向複合,由於在示意圖裏,函子一般是往下堆砌的。豎向複合對於定義函子範疇很重要。下面我簡短介紹一下橫向複合。

豎向複合與橫向複合

範疇 C 與 D 之間的函子範疇記爲 Fun(C, D)[C, D],有時也寫成 D^C。最後這種記法暗示了可將函子範疇自己視爲其餘範疇裏的一個函數對象(指數)。其實是這樣嗎?

看一下咱們到如今爲止所構建的抽象層。咱們從一個範疇開始,它由一組對象與態射構成。範疇自己(或嚴格地說是小范疇,它們的對象造成集合)是更高層的範疇 Cat 裏的對象。在 Cat 裏,態射是函子。Cat 裏的 Hom-集是函子構成的集合。例如,Cat(C,D) 是範疇 C 與 D 之間的函子集合。

Cat 範疇

函子範疇 [C, D] 也是兩個範疇之間的函子集合(加上天然變換爲態射)。它裏面的對象也是 Cat(C,D) 裏的東西。此外,函子範疇是範疇,它自己必須得是 Cat 裏面的對象之一(也就是說,兩個小范疇之間的函子範疇自己也很小)。一個範疇裏的 Hom-集與同一個範疇裏的對象之間存在聯繫。這種狀況就像咱們在上一節裏所看到的指數形式的對象。如今來看一下,Cat 裏如何構造後者。

你可能還記得,爲了構造一個指數,須要首先定義積。在 Cat 裏,定義積至關容易,由於小范疇是對象的集合,而咱們又知道怎樣定義集合的笛卡爾積。所以,積範疇 C × D 裏的一個對象,是兩個對象構成的序對 (c, d),一個來自 C,一個來自 D。相似地,在這樣的序對 (c, d)(c', d') 之間的態射是一個態射序對 (f, g),其中 f :: c -> c'g :: d -> d'。因爲這些態射序對由 CD 中態射組成,所以老是會有一個由 CD 中的恆等態射構成的序對。長話短說,Cat 是一個徹底的笛卡爾閉範疇,對於任意一對範疇(譯註:例如 CD),它裏面存在着相應的指數對象 D^C。因爲我說過, Cat 裏的對象是範疇,所以 D^C 是範疇,它就是 CD 之間的函子範疇。

2-範疇

問題解決了,咱們如今近觀一下 Cat。根據定義,Cat 裏的任意 Hom-集都是函子集合。可是,就像咱們見識過的,兩個對象之間的函子有着比集合更豐滿的結構。它們造成一個範疇,以天然變換爲態射。因爲在 Cat 裏,函子被認爲是態射,天然變換就是態射之間的態射。

這個更豐滿的結構是 2-範疇的一個例子。2 -範疇是一個廣義的範疇,其中,除了對象和態射(這裏應該叫它 1-態射)以外,還有 2-態射,它就是態射之間的態射。

Cat 的 2-範疇具備:

  • 對象:(小)範疇
  • 1-態射:範疇之間的函子
  • 2-態射:函子之間的天然變換

咱們用 Hom-範疇——函子範疇 D^C 來代替範疇 CD 之間的 Hom-集。咱們有常規的函子複合:來自 D^C 的函子 F 與來自 E^D 的函子 G 複合,能夠獲得來自 E^C 的函子 G ∘ F。可是,在每一個 Hom-範疇內部,也存在着複合——函子之間天然變換或 2-態射的豎向複合。

豎向複合

使用 2-範疇裏的兩種複合方法,問題升級爲:它們之間有何關係?

咱們先選在 Cat 裏選兩個函子,或者 1-態射:

F :: C -> D
G :: D -> E

與它們的複合:

G ∘ F :: C -> E

假設咱們有兩個天然變換,αβ,它們分別做用於函子 FG

α :: F -> F'
β :: G -> G'

注意,咱們不能對這兩個天然變換應用豎向複合,由於 α 的終點與 β 的始點不重合。實際上,它們分別屬於兩個不一樣的函子範疇 D^CE^D。不過,咱們可以複合函子 F'G',由於 F' 的終點與 G' 的起點重合——它就是範疇 D。函子 G’∘ F’G ∘ F 之間有什麼關係呢?

如今咱們手裏有 αβ,可不能夠定義一個從 G ∘ FG’∘ F’ 的天然變換?咱們畫個草圖看看:

往常,咱們從 C 中的一個對象 a 開始。它分裂爲兩個 D 中的對象:F aF' a。還有一個態射,α 的一個份量,鏈接這兩個對象:

α_a :: F a -> F'a

在從 DE 的時候,這兩個對象進一步分裂爲四個對象:

G (F a), G'(F a), G (F'a), G'(F'a)

咱們還有 4 個態射,它們造成了一個方格。這些態射中有兩個是天然變換 β 的份量:

β_{F a} :: G (F a) -> G'(F a)
β_{F'a} :: G (F'a) -> G'(F'a)

另外兩個則是 α_a 在兩個函子下的圖像(函子映射了態射):

G α_a :: G (F a) -> G (F'a)
G'α_a :: G'(F a) -> G'(F'a)

好多態射。咱們的目標是尋找從 G (F a)G'(F'a) 的態射。一個候選解是鏈接兩個函子 G ∘ FG’∘ F’ 的天然變換的份量。事實上,從
G (F a)G'(F'a) 的路徑不是一條,而是兩條:

G'α_a ∘ β_{F a}
β_{F'a} ∘ G α_a

幸虧,它們相等。由於這四個態射所造成的方格對於 β 而言具備天然性。

咱們剛纔已經定義了從 G ∘ FG’∘ F’ 的天然變換的一個份量。假若你足夠有耐心,那麼這個變換的天然性證實至關直觀。

咱們將這個天然變換稱爲 αβ 的橫向複合:

β ∘ α :: G ∘ F -> G'∘ F'

再一次沿用 Mac Lane 的記法,我使用小圓圈來表示橫向複合。在它出現的位置上,你也可能看到的是星號。

有一個範疇化的經驗法則:每次拿到複合時,應該去找一個範疇。咱們有天然變換的豎向複合,它是函子範疇的一部分。那麼,橫向複合呢?它身居什麼範疇裏?

要獲得答案,須要從側面來看 Cat。不要將天然變換當作函子之間的箭頭,而是將它們當作範疇之間的箭頭。一個天然變換位於兩個範疇之間,而這兩個範疇本來是由這個天然變換所變換的函子鏈接的。咱們能夠認爲這個天然變換鏈接着這兩個範疇。

如今,咱們把注意力放在 Cat 裏的兩個對象上,即範疇 CD。存在着由天然變換構成的集合,這些天然變換來往於鏈接 CD 的函子之間。這些天然變換就是咱們從 CD 的新箭頭。同理,也有一些天然變換來往於鏈接 DE 的函子之間的天然變換,咱們將它們視從 DE 的新箭頭。橫向複合,就是這些箭頭的複合。

咱們也有一個從 CC 的恆等箭頭。它是 C 上的恆等函子自身的恆等天然變換。注意,橫向複合的恆等也是豎向複合的恆等,可是反過來卻不是。

最後,這兩種複合知足交換律:

(β' ⋅ α') ∘ (β ⋅ α) = (β' ∘ β) ⋅ (α' ∘ α)

在此,我引用 Saunders Mac Lane 的說法:讀者可能以爲繪製顯而易見的示意圖要比去證實它更有趣。

之後還會有更多的記法。在這個從側面看 Cat 的新解釋裏,從一個對象到另外一個對象存在兩種方法:使用函子或使用天然變換。然而,咱們能夠將函子箭頭從新解釋爲一種特殊的天然變換:恆等天然變換做用於這個函子。所以,你將會常常遇到這種記號:

F ∘ α

其中,F 是從 DE 的函子,而 α 是從 CD 的兩個函子之間的天然變換。由於你不能將用一個天然變換去與一個函子進行復合,因此這個記號須要解讀爲恆等天然變換 1_F 位於 α 以後的橫向複合。

相似地:

α ∘ F

α 位於 1_F 以後的橫向複合。

總結

這是對這本書第一部分的總結。咱們已經瞭解了範疇論的基本術語。你可能會這樣認爲:對象與範疇是名詞;態射、函子以及天然變換是動詞。態射鏈接了對象,函子鏈接了範疇,天然變換鏈接了函子。

可是咱們已經看到了,一個抽象層上的一個動做,在下一個抽象層次上就變成了一個對象。態射的集合變成了函數對象。做爲對象,它能夠是另外一個態射的始點或終點。這就是高階函數背後的思想。

函子,將對象映射爲對象,所以咱們將其做爲類型構造子,或者做爲一種參數化的類型。函子,也能將態射映射爲態射,所以它也是高階函數——fmap。有一些簡單的函子,例如 Const、積以及餘積,它們能夠產生大量的代數數據類型。函數類型也具備函子性,協變性與逆變性,它們能夠用於擴充代數數據類型。

函子在函子範疇裏能夠視爲對象。這樣,它們就變成了態射的始點與終點,因而有了天然變換。天然變換就是特定形式的多態函數。

挑戰

  1. 定義從 Maybe 到列表函子的天然變換,並證實它符合天然性條件。
  2. Reader () 與列表函子構造至少兩個不一樣的天然變換。存在多少個不一樣的 () 列表?
  3. Reader BoolMaybe 來作上一個練習。
  4. 揭示天然變換的橫向複合知足天然性條件(提示:使用份量)。對於追求示意圖的人而言,這是個很好的練習。
  5. 寫一篇文章,談談你是如何以爲畫顯而易見的示意圖賽過證實交換律。
  6. 爲不一樣的 Op 函子之間的變換的相反天然性條件,建立一些測試案例。如下是一個示例:
op :: Op Bool Int
op = Op (\x -> x > 0)

f :: String -> Int
f x = read x

致謝

感謝 Gershom Bazerman 檢查了個人數學和邏輯,也感謝 André van Meulebrouck 在編輯方面的幫助。

$$ \cdot $$

譯註:做者後面還有兩部份內容,可是我決定只翻譯到這裏。另外,這篇文章的原文下面的評論區,一位網名「benjaminy」的人的評論,也值得思考。另外,做者在這第一部分所講述的這些範疇論概念,已經足以讓你在必定程度上了解單子——自函子範疇上的一個幺半羣。

相關文章
相關標籤/搜索