上一篇:自由幺半羣編程
原文地址:https://bartoszmilewski.com/2...segmentfault
是時候談談集合了。數學家們對集合論是又愛又恨。它是數學中的彙編語言——至少它經常是。範疇論在某種程度上嘗試跳出集合論,一個衆所周知得事實就是不存在全部集合的集合,但全部集合的範疇,Set,是存在的。這就很好。另外一方面,咱們假定一個範疇中任意兩個對象之間的態射構成一個集合。咱們還叫它hom集。爲了公平,還有一種範疇論中態射並不構成集合。取而代之的是它們是另外一個範疇中的對象。這些範疇使用的不是hom集而是hom對象,它們被稱做富範疇。然而,接下來,咱們還將只看那些使用可愛的原始形式的hom集的範疇。數據結構
富範疇的原文爲enriched category,我沒有找到它對應的中文。譯者注。
集合是你能找到的最接近範疇對象的平凡的傢伙了。一個集合有元素,但你不能對這些元素說更多的事。若是你有一個有限集,那麼你能數出他們來。你能夠用基數大體對無限集的元素計數。好比,天然數集小於實數集,即便它們都是無限多的。可是,可能有些讓人驚訝的是,有理數集和天然數集同樣大。ide
除此以外,全部有關集合的信息都能表如今它們之間的函數上——尤爲是叫作同構的那些可逆的傢伙。同構的集合在任何意義下都是徹底同樣的。在我引發基礎數學家們的憤怒以前,讓我解釋一下:相等和同構的區別具備很是根本的重要性。實際上它是數學最新的分支,同倫類型論(the Homotopy Type Theory ,HoTT)關心的主要問題之一。我提到HoTT是由於它是靈感來源於計算的一門純粹的數學理論,而它主要的支持者之一,Vladimir Voevodsky,主要是在研究Coq定理證實輔助器時頓悟的。數學和編程的互動是雙向的。函數
關於集合的重要的一課是,不想元素那樣,集合是能夠比較的。好比,咱們能夠說一個給定的天然變換的集合同構於某個態射的集合,由於一個集合就只是一個集合。在這個例子裏同構就只是說對於一個集合裏的每一個天然變換另外一個集合裏都有惟一的一個態射與之對應,反之亦然。他們能夠互相配對。若是蘋果和橘子是不一樣的範疇裏的對象,那你不能比較蘋果和橘子,但你能夠比較蘋果的集合和橘子的集合。一般把一個範疇問題轉換成一個集合論的問題會給咱們一些必要的直觀或者甚至讓咱們證實有價值的定理。post
每一個範疇都天生具備一個到Set的典型映射族。這些映射其實是函子,因此它們維持範疇的結構。讓咱們構造一個這樣的映射。性能
咱們固定C的一個對象a
而後選擇另外一個對象x
,hom集C(a, x)
是個集合,也就是Set的一個對象。當咱們保持a
固定不變而變化x
時,C(a, x)
也會在Set中變更。所以咱們有了個從a
到Set的映射。spa
若是咱們想強調咱們正把hom集看做以它的第二個參數做自變量的映射,就使用記號:翻譯
C(a, -)
其中鏈接號充當了該參數的佔位符。3d
對象的映射能夠容易地拓展到態射的映射。咱們取C中兩個任意對象x
和y
的態射f
。在咱們剛剛定義的映射下,對象x
被映爲集合C(a, x)
而y
被映爲C(a, y)
。若是該映射要成爲一個函子,f
必須被映爲這兩個集合之間的一個函數:
C(a, x) -> C(a, y)
讓咱們逐點定義這個函數,逐點就是分別對每一個取值分別處理。這裏咱們應該選取C(a, x)
中的一個任意元素——咱們叫它h
好了。首尾相連的態射是可複合的。h
的尾和f
的頭就是這種匹配的狀況,因此它們的複合:
f ∘ h :: a -> y
是一個a
到y
的態射。所以它是C(a, y)
的一個傢伙。
咱們剛剛找到了從C(a, x)
到C(a, y)
的函數,它是f
的像。若是不至於引發歧義,咱們把這個提高後的函數寫做:
C(a, f)
它在態射h
上的行爲是:
C(a, f) h = f ∘ h
因爲在任意範疇裏均可以這樣構造,它確定也能夠在Haskell類型範疇中實現,這個hom函子就是衆所周知的Reader
函子:
type Reader a x = a -> x
instance Functor (Reader a) where fmap f h = h . h
如今咱們考慮一下,若是把固定hom集的源點改成固定靶點,會發生什麼。換句話說,咱們問是否映射
C(-, a)
也是個函子。它是,但它再也不是協變的,它是逆變的。這是由於一樣的首尾相連的態射的配對會致使f
後複合而不是C(a, -)
的那種前複合。
前複合對應的英文爲precomposition,後複合對應的英文爲postcomposition,f
前複合就是說複合時f
在前,f
後複合就是說複合時f
在後。
咱們已經看到了Haskell中的這個逆變函子。咱們叫它Op
:
type Op a x = x -> a
instance Contravariant (Op a) where contramap f h = h . f
最後,若是咱們讓兩個對象均可變,就獲得了逆變協變函子(profunctor)C(-, =)
,它的第一個參數是逆變的,第二個參數是協變的(爲了強調兩個參數能夠獨立地變化,咱們用雙鏈接號做爲第二個佔位符)。咱們以前已經看過這個逆變協變函子了,是在咱們講到函子性的時候:
instance Profunctor (->) where dimap ab cd bc = cd . bc . ab lmap = flip (.) rmap = (.)
在第一部分的翻譯中,profunctor被譯爲「副函子」,我認爲不妥,因而找到了逆變協變函子這樣的叫法。譯者注。
重要的教訓是這個觀察在任意範疇都成立:把對象映爲hom集是具備函子性的。既然逆變性等價於一個反範疇的映射,咱們就能夠把這件事簡寫爲:
C(-, =) :: C^op x C -> Set
咱們已經看到,選擇C中的每個對象a
,咱們得到一個從C到Set的函子。這種指向Set的結構保持的映射一般被稱爲一個表示。咱們把C中的對象和態射表示爲Set的集合和函數。
函子C(a, -)
自己一般說是可表的。更通常地,任意與選擇了某個a
的hom函子天然同構的函子F
被稱做可表的。這種函子必定是指向Set的,由於C(a, -)
指向Set。
我以前說過咱們常常把同構當作同一的。更通常地,咱們把一個範疇中同構的對象看做同一的。這是由於對象除了到其餘對象(和他們本身)的態射關係外沒有其餘的結構了。
好比說,咱們以前談到過幺半羣範疇,Mon,它最開始就是用集合建模的。可是咱們很當心地選取了那些保持了集合的幺半羣結構的函數做爲態射。因此若是Mon的兩個對象是同構的,意味着它們之間有一個可逆的態射。它們精確地具備相同的結構。若是咱們看看這些態射所基於的集合和函數,咱們將會看到一個幺半羣的單位元被映射到了另外一個的單位元,而且兩個元素的積被映射爲它們的像的積。
一樣的推斷能夠用在函子上。兩個範疇間的全部函子構成了一個範疇,而天然變換扮演了態射的角色。因此若是在兩個函子間存在可逆的天然變換,那麼它們是同構的,而且可以被視爲同一的。
讓咱們從這種視角分析一下可表函子的定義。由於F
是可表的,咱們須要:有C中的一個對象a
;一個從C(a, -)
到F
的天然變換α
;另外一個反過來的天然變換β
;而且它們的複合是恆等天然變換。
讓咱們看看α
在某個對象x
上的份量。這是一個Set中的函數:
α_x :: C(a, x) -> F x
這個變換的天然性條件告訴咱們,對於任意從x
到y
的態射f
,下面的四方圖是交換的:
F f ∘ α_x = α_y ∘ C(a, f)
在Haskell中,咱們能夠用多態函數代替天然變換:
alpha :: forall x. (a -> x) -> F x
其中有可選的forall
量詞。因爲參數化多態(這是一個我以前提到的免費定理的一個),天然性條件
fmap f . alpha = alpha . fmap f
會自動知足。注意,左式的fmap
是定義在函子F
上的,而右邊的那個是定義在reader函子上的。由於reader的fmap
就只是作了函數前複合,咱們甚至能夠再精確些。做用在C(a, x)
的一個元素h
上時,天然性條件簡化爲:
fmap f (alpha h) = alpha (f . h)
另外一個變換β
是反方向走的:
beta :: forall x. F x -> (a -> x)
它必須遵照天然性條件,而且它必須是α
的逆:
α ∘ β = id = β ∘ α
咱們以後將會看到從C(a, -)
到任意指向Set的函子的天然變換總會存在(米田引理),但它不必定可逆。
讓我給你個Haskell的例子吧——列表函子而且用Int
做爲a
。這裏是能實現這件事的一個天然變換:
alpha :: forall x. (Int -> x) -> [x] alpha h = map h [12]
我任取了數字12而且用它建立了個單例列表。接着我就能在這個列表上fmap
函數h
獲得一個h
返回值類型的列表。(實際上這種變換的數目和整數列表的數目同樣多。)
天然性條件就等價於map
(fmap
的列表版本)的可複合性:
map f (map h [12]) = map (f . h) [12]
可是要是咱們試圖尋找逆變換,咱們不得不把任意類型x
的列表變成一個返回x
的函數:
beta :: forall x. [x] -> (Int -> x)
你可能會考慮從列表中檢索出一個x
,好比,用head
,但它不能應用在空列表上。注意沒有哪一個a
的選擇(以代替Int
)可讓它工做。因此列表函子並非可表的。
還記得咱們說過Haskell函子有點像容器嗎?一樣地咱們能夠把可表函子看做把函數調用(hom集的成員在Haskell中僅僅就是函數)後的憶存結果存儲起來的容器。表示對象,也就是C(a, -)
裏的類型a
被看做關鍵字類型,用它咱們能夠獲得一個函數的表值。咱們所稱做α
的變換叫tabulate
,它的逆,β
,叫index
。這是一個(略微簡化的)Representable
類的定義:
class Representable f where type Rep f :: * tabulate :: (Rep f -> x) -> f x index :: f x -> Rep f -> x
憶存一詞英文爲"memoize",我沒有找到相應的中文。它專指計算機領域將函數的運行結果保存下來,下次調用時直接取出而不從新計算的加速方法。
注意表示類型,也就是咱們的a
,這裏被叫作Rep f
,是Representable
定義的一部分。星號只是說Rep f
是個類型(而不是類型構造子,或者其餘更奇怪的)
無限列表,或者叫流,是不能夠爲空的,它是可表的。
data Stream x = Cons x (Stream x)
你能夠把他們當作一個接受Integer
參數的函數的憶存值。(嚴格地講,我應當用非負天然數,但我不想讓個人代碼更復雜。)
爲了tabulate
這樣一個函數,你得創造一個值的無限流。固然,這能作到僅僅是由於Haskell是惰性的。值只有在須要時才被求值。你能夠用index
獲得憶存值。
instance Representable Stream where type Rep Stream = Integer tabulate f = Cons (f 0) (tabulate (f . (+1))) index (Cons b bs) n = if n == 0 then b else index bs (n-1)
這頗有趣,你能夠只實現一個憶存表就覆蓋任意返回類型的函數的族。
逆變函子的可表性也是相似定義的,只不過咱們固定了C(-, a)
的第二個參數。或者等價地說,咱們能夠考慮從C_op
到Set的函子,由於C_op(a, -)
就是C(-, a)
。
可表性有個有趣的變形。回憶hom集能夠在笛卡爾閉範疇裏被當作指數對象。hom集C(a, x)
就等價於x_a
,而且一個可表函子F
咱們能夠寫成:
-_a = F
讓咱們兩邊取對數,這只是隨便看看:
a = log F
固然,這只是個純粹的公式變換,但若是你知道些對數的性質,那就會頗有用了。尤爲是,能夠證實做用於積類型的函子能夠表示成和類型,而和類型的函子並不都是可表的(例子:列表函子)。
最後,注意到一個可表函子給咱們提供了一樣一件事情的兩種不一樣實現——一種是函數,一種是數據結構。它們有着徹底相同的內容——一樣的值會被一樣的關鍵字檢索到。這就是我以前談到的「同一」的意思。只要兩個天然同構的函子所涉及的內容是是同一的,那它們就是同一的。另外一方面,這兩種表示方式常常會用不一樣方式實現所以可能有徹底不一樣的性能。憶存被用來提高性能因此可能使運行時間大大縮減。在實踐中,能對相同的隱性計算過程創造不一樣的表達方式是很是有價值的。因此,很讓人驚喜的是,即便如今並無關心性能,範疇論也爲探索其餘可能的有實際價值的實現提供了足夠的機會。
Maybe
不是可表的。Reader
函子可表嗎?Stream
的表示,憶存平方函數。Stream
的tabulate
和index
確實是互逆的。(提示:使用概括法)函子:
Pair a = Pair a a
是可表的。你能不能猜到表示它的類型是什麼?實現tabulate
和index
。
感謝Gershom Bazerman檢查個人數學和邏輯,以及André van Meulebrouck在整個系列中的編輯上的幫助。
下一篇:米田引理