<譯>米田引理

上一篇：可表函子

原文地址：https://bartoszmilewski.com/2...

範疇論中的大多數構造都是其餘具體數學領域的泛化。諸如積、餘積、幺半羣和指數等等，早都在範疇論之前被瞭解了。在不一樣的數學分支中，它們也許有不一樣的名字。集合論中的笛卡兒積，序數理論的下确界，邏輯中的連詞——他們都是範疇積這樣一個抽象觀點的具體例子。

但做爲一個有關範疇的通常陳述，米田引理卻徹底不一樣。它少有或沒有其餘數學分支中的先例。有些人說與它最靠近的類比是羣論中的凱萊定理（每一個羣都同構於某個集合的置換羣）。

米田引理的設定是一個任意範疇C和一個從C到Set的函子F。咱們已經在以前的部分看到過一些指向Set的函子是可表的，也就是同構於一個hom函子。米田引理是說全部指向Set的函子都能經過天然變換從hom函子得到，並且米田引理精確的列舉了全部這樣的變換。

在討論天然變換的時候，我曾說過天然性條件可能很是嚴格。當你定義一個天然變換在一個對象上的份量的時候，天然性得強到能夠把這個份量「搬」到另外一個對象的份量上，而這另外一個對象和原對象有態射鏈接。源範疇和靶範疇的箭頭越多，你要搬運天然變換的份量的限制就越多。Set碰巧就是一個箭頭很是多的範疇。

米田引理告訴咱們，一個hom函子和任意其餘函子F間的天然變換被它的單個份量在一個點的取值徹底決定！這個天然變換剩下的部分僅僅遵循天然性條件。

因此讓咱們再來看看米田引理所用到的兩個函子間的天然性條件吧。第一個函子是hom函子。它把C的任意對象x映爲態射的集合C(a, x)——a是C中的一個固定對象。咱們也已經看到過它把任意x到y的態射f映爲C(a, f)。

第二個函子是任意指向Set的函子F。

讓咱們把這兩個函子間的天然變換稱做α。由於咱們是在Set中操做，像α_x或α_y這樣的天然變換份量就只是常規的集合間的函數：

α_x :: C(a, x) -> F x
a_y :: C(a, y) -> F y

而由於這些都是函數，咱們就能夠看看它們在具體點上的值。但集合C(a, x)裏的點是什麼？這就是關鍵的觀察了：集合C(a, x)的每一個點也是個從a到x的態射h。

因此α的天然性四方圖：

α_y ∘ C(a, f) = F f ∘ α_x

逐點做用在h上時，就變成了：

α_y (C(a, f) h) = F f (α_x h)

你能夠從以前的部分回想起hom函子C(a, -)在態射f上的行爲就被定義爲前複合：

C(a, f) h = f ∘ h

這就導出了：

α_y (f ∘ h) = (F f) (α_x h)

這個條件究竟有多強看看讓x等於a的情形就知道了。

這時h變成了一個從a到a的態射。咱們知道至少存在一個這樣的態射，h = id_a。讓咱們把它帶入：

α_y f = (F f) (α_a id_a)

注意發生了什麼：左邊是α_y在C(a, y)的任意元素f上的做用。而且它由α_a在id_a的這單單一個值所徹底決定。咱們能夠任意選取這樣的值，這樣就生成了一個天然變換。由於α_a的值落在集合F a中，因此F a的任意點都定義了某個α。

反過來，給定任意從C(a, -)到F的天然變換α，你能夠計算出它在id_a的值，從而獲得一個F a的點。

這樣咱們就證實了米田引理：

從 C(a, -)到 F的天然變換和 F a的元素是一一對應的。

換句話說，

Nat(C(a, -), F) ≅ F a

或者說，若是咱們用記號[C, Set]表示C和Set間的函子範疇，天然變換的集合就只是這個範疇的一個hom集了，而且咱們能夠寫成：

[C, Set](C(a, -), F) ≅ F a

這個對應其實是個天然同構，我以後會解釋這是怎麼回事。

如今讓咱們試着直觀感覺下這個結果。最讓人驚訝的莫過於整個天然變換從一個凝結點開始結晶了：凝結點就是天然變換做用於id_a的值。在天然性條件下，天然變換從該點向外延伸。它覆蓋了Set中全部C的像。因此咱們首先考慮下C在C(a, -)的像。

讓咱們從a本身的像開始。在hom函子C(a, -)下，a被映爲集合C(a, a)。另外一方面，在函子F下，它被映爲集合F a。天然變換的份量α_a是某個從C(a, a)到F a的函數。讓咱們僅僅關注C(a, a)的一個點，也就是那個對應於態射id_a的點。爲了強調它只是集合中的一個點，咱們把它叫作p。份量α_a應當把p映爲F a的某個點q。我將給你證實任意q的選擇會導出惟一的天然變換。

第一個斷言是q的選擇會惟一決定函數α_a的剩餘部分。真的，讓咱們任選C(a, a)的另外一個點p'，它對應某個從a到a的態射g。接下來就是米田引理的魔法時刻了：g能夠被當作集合C(a, a)的某個點p',同時它還對應着兩個集合間的函數。確實，在hom函子下，態射g被映爲函數C(a, g)；在F下它被映爲F g。

如今咱們考慮C(a, g)在咱們原始的p上的做用，p就是對應着id_a的那個傢伙。這定義成前複合，g∘id_a，它就是g，也對應着咱們的點p'。因此態射g被映爲了一個把p映爲p'的函數，而p'就是g。咱們整整兜了一圈！

如今考慮F g在q上的做用。這會是某個q'，F a的一個點。爲了補全天然四方圖，p'必須在α_a下被映爲q'。咱們選取了任意的p'(也就是任意的g)而後獲得了它在α_a下的像，所以函數α_a徹底肯定了。

第二個斷言是對於C中的任意和a有鏈接的對象x，α_x會被惟一決定。緣由是相似地，只不過如今咱們多了兩個集合C(a, x)和F x，而且從a到x的態射g在hom函子下被映爲了：

C(a, g) :: C(a, a) -> C(a, x)

而在F下被映爲：

F g :: F a -> F x

一樣地，C(a, g)在咱們的p上的做用由前複合給出：g ∘ id_a，這對應了C(a, x)的一個點p'。天然性決定了α_x做用在p'上的值會是：

q' = (F g) q

由於p'是任取的，因此所以整個α_x被肯定了。

若是C中有和a沒有鏈接的對象呢？它們在C(a, -)下會通通被映爲一個集合——空集。回憶一下，空集是集合範疇的初始對象。這意味着從它到任意其餘集合只有一個函數。咱們曾把它叫作absurd。因此一樣地，咱們仍然沒有選擇天然變換份量的餘地：它只能是absurd。

一個理解米田引理的方法是把指向Set的函子間的天然變換們就看做一堆函數族，而函數一般是會損失信息的。一個函數可能會坍縮信息，而且它可能只覆蓋上域的一部分。那些僅有的不會損失信息的函數就是那些可逆函數——同構。所以呢，最好的保持結構的指向Set的函子就是那些可表的。它們或者是hom函子，或者和hom函子天然同構。任何其餘從hom函子獲得函子F的過程都損失了信息。這樣的變換可能不止損失了信息，它也可能只覆蓋了函子F在Set上像的一小部分。

Hasekll中的米田引理

咱們已經遇到過Haskell中假裝成reader函子的hom函子了：

type Reader a x = a -> x

reader經過前複合映射態射（這裏就是函數）：

instance Functor (Reader a) where
    map f h = f . h

米田引理告訴咱們reader函子能夠被天然地映爲其餘函子。

一個天然變換就是一個多態函數。因此給定一個函子F，咱們就有一個由reader函子到它的映射：

alpha :: forall x . (a -> x) -> F x

一般來講，forall是能夠省略的，但我想把它明確地寫出來以強調天然變換的參數化多態性質。

米田引理告訴咱們這些天然變換和F a的元素們一一對應：

forall x . (a -> x) -> F x ≅ F a

這個等價的右邊通常被看做一個數據結構。還記得把函子看做容器的推廣的解釋嗎？F a是一個a的容器。但左邊是個以一個函數做爲參數的多態函數。米田引理說這兩種表達等價——它們包含了一樣地信息。

另外一個說法是：給我一個這種類型的多態函數：

alpha :: forall x . (a -> x) -> F x

我就能獲得一個a的容器。技巧就是咱們以前在米田引理的證實中用到過的：咱們用id調用這個函數就獲得了F a的一個元素：

alpha id :: F a

反過來也對。給定一個F a的值：

fa :: F a

就能夠定義一個恰當類型的多態函數：

alpha h = fmap h fa

你能夠輕易地在這兩種表達間來回切換。

多種表達的好處是其中一種可能比另外一種易於複合，或者某些應用中一種可能比另外一種更有效率。

這個原理地最簡單示例就是常常用在編譯器構造中地編碼轉換：延繼傳遞風格或CPS。這是米田引理在恆等函子上最簡單的應用。把F換成恆等函子就獲得了：

forall x . (a -> r) -> r ≅ a

關於延繼傳遞風格（Continuation-passing style，CPS），網上的叫法不一，但大多把continuation譯爲「延續」，我以爲不妥。由於在CPS中，把須要傳遞的類型爲 (a -> r)的函數就叫the continuation。稱呼一個函數爲延續畢竟有些口語，不符合數學的習慣，因而我就自做主張的譯爲「延繼」了。譯者注。

這個公式的解釋是任意類型a能夠被代替成一個以一個a的「處理器」爲參數的函數。一個處理器就是一個接受a爲參數並執行後續計算的函數——延繼。（類型r一般封裝成某種類型的狀態碼）

這種編程風格在用戶界面編程、異步系統和並行編程中都很是廣泛。CPS的缺點是它設計了控制的反向。開發端和用戶（處理器端）的代碼是分離的，這就不易於複合。誰要是作過些通常的web編程，就會了解交互式狀態處理程序的麪條代碼的噩夢了。就像咱們以後會看到的，若是函子和單子使用得當，就能存儲一些CPS的可複合性質了。

逆米田引理

就像以往同樣，咱們經過將箭頭反向獲得了額外的構造。米田引理能夠應用到反範疇C_op從而給出逆變函子間的映射。

等價的說，咱們經過固定hom函子的靶對象而不是源對象獲得了逆米田引理。咱們獲得從C到Set的逆變hom函子：C(-, a)。米田引理的這個逆變版本構建了這個函子到其餘任意逆變函子F間的天然變換與集合F a的元素之間的一一對應：

Nat(C(-, a), F) ≅ F a

這兒是逆米田引理Haskell版本：

forall x . (x -> a) -> F x ≅ F a

注意，有些文獻中把這個逆變版本就叫米田引理。

挑戰

1. 證實這兩個在Haskell中組成米田同構的函子phi和psi互逆。

   phi :: (forall x . (a -> x) -> F x) -> F a
   phi alpha = alpha id

   psi :: F a -> (forall x . (a -> x) -> F x)
   psi fa h = fmap h fa

2. 所謂離散範疇就是指有一些對象，但除了恆等態射外沒有別的態射的範疇。米田引理是如何處理從這個範疇出發的函子的？
3. unit的列表[()]除了它的長度不包含任何其餘信息。因此，做爲一個數據類型，它能夠視爲整數的一個編碼方式。空列表表明0，單例列表[()](這是一個值，並非類型)表示1，等等。請使用米田引理構造出這個列表函子的另外一種表示。

參考文獻

1. Catsters video

致謝

感謝Gershom Bazerman檢查個人數學和邏輯，以及André van Meulebrouck在整個系列中的編輯上的幫助。

下一篇：米田嵌入