如何理解Monad are just free monad monad monad algebras

時間 2021-05-30 11:59:56

1樓:BigGT

我看了題主給的鏈結裡的原文,感覺應該沒有很複雜。如果有乙個adjunction (+blabla條件),那麼 。現在考慮 , ,即範疇 上的monad和endofunctor的category,那麼,其中的 就是free monad。

所以說 上的monad就是free-monad()這個monad的monad-algebra。

2樓:「已登出」

感覺作者是想說 Monad is action of a cat on set:

action in nLab

action of a category on a set in nLab

感覺主要是因為 monad 的 monoid 性質

3樓:張智浩

看起來這句話是想湊個文字遊戲的感覺。本來我是給這句話斷句都不能的,但是看了看題主自己的回答,好歹是知道啥意思了。我沒仔細看文章,主要是 Haskell 確實不懂(雖然曾經想要學一學)。

目前已有的答案其實已經說得比較清楚了,我這就補充一些細節之類的吧。但是為了完整性,還是寫得正式一點,也算是自己的乙個總結。

(但寫完才發現關鍵的證明細節我也沒寫,畫圖追圖什麼的太繁瑣了;我就寫了下大致思路和一些關鍵點,應該能跟著走下去)

零、開篇隨便說兩句

一、Monad 差不多就是伴隨函子

二、什麼時候伴隨函子的 monad-algebra 「是好的」

三、為什麼 free-monad monad monad-algebra 是 monad

首先假定讀者知道 monad 是什麼,當然為了完整性我們還是重複一下定義:設 是乙個範疇,那麼 上的乙個 monad 就是乙個三元組 ,有時也省略後面兩個自然變換而只用第乙個函子 來標記。

也可以用另一種等價的方式來表述:考慮所有 的函子和它們之間的自然變換組成的範疇 ,這是乙個 (strict) monoidal category,那麼其上的 monoid(或者也叫 algebra)就是 monad。

但這種說法除了看起來「厲害」一些之外並沒有顯得特別有用——如果是這樣的話,我們豈不是只要研究 monoidal category 就好了,為啥還要研究 monad?(但事實上到最後我們還是會用到這個說法)

(2023年更新一波:這個厲害的說法還有進一步的版本,即乙個 monad-algebra 其實是這個 monad——視為函子範疇裡的代數——在原範疇——視為函子範疇的左模——裡面的左模。以前我覺得這些說法除了看起來厲害意義不大,但現在我的看法可能會有一些變化:

它告訴我們表示論無處不在。或許我們暫時不知道從這種說法能直接得到什麼,但僅僅是把 monad theory 和表示論聯絡了起來,我覺得這就很不得了了)

我也說不出很多東西來,但至少 monad 與伴隨函子有很密切的聯絡。前兩節主要(試圖)澄清這一聯絡,第三節回到 free-monad monad monad-algebra 的具體問題上。

主要參考文獻是 Emily Riehl 的Category Theory in Context,基本前兩節是照搬這本書。

(為了好看,以下態射的復合用 而不是 來表示;此外很多交換圖很難畫,所以我乾脆乙個都不畫了)

設 是兩個範疇而 是一對伴隨函子。作為例子,我們可以考慮 是集合範疇而 是某個代數結構的範疇,比如帶點集合、么半群、群、阿貝爾群之類的,然後 是遺忘函子而 是自由函子。

作為伴隨函子,我們有 unit 和 counit 的自然變換,即 和 。神奇的是,我們立馬可以從這裡得到乙個 上的 monad:定義 ,然後 就是上面伴隨函子的 ,而 就定義為 (雖然這個記號可能有些奇怪)。

換句話說,如果我只是「站」在 上來看,那麼 上的東西是看不到的,這兩個函子也看不到,但上述三者是可以看到的,它們構成乙個 monad。於是乙個「自然」的問題是:我從 和這個 monad 出發,可以把 和這一對伴隨函子給恢復出來嗎?

所謂 monad-algebra 的概念算是部分回答了這個問題。

Definition.設 是範疇 上的乙個 monad,乙個 -algebra 是乙個二元組 ,這裡 是 中的乙個物件而 是 中的乙個態射,且滿足

從 到 之間的 -algebra morphism 是乙個 中的態射 使得 。

這樣得到的所有 -algebra 的範疇記為 。顯然有遺忘函子 把 送到 ,而另一方面有自由 -algebra 函子 把 送到自由 -algebra 。(這兩個函子在態射上的作用比較顯然,不寫了)

神奇的事情發生了:這一對函子 是一對伴隨函子,並且這一對伴隨函子產生的 monad 就是 本身。

證明不太困難,簡單說一下:我們只需要找 unit 和 counit 驗證即可,這裡 unit 就是 自帶的 unit,而 counit 就由 給出。

可以簡單驗證一些簡單的例子裡面這些 monad-algebra 是什麼。正如另乙個答案所驗證過的那樣,集合-阿貝爾群之間的 monad 產生的 monad-algebra 就是阿貝爾群。同樣一開始說過的那些代數結構的例子都可以驗證一下,其 monad-algebra 都回到代數結構本身。

此外,那一對伴隨函子也是我們所期待的自由-遺忘伴隨函子。

於是自然會想:也許 monad 其實就是伴隨函子,我們已經知道伴隨函子能產生 monad,並且 monad 通過 monad-algebra 也能產生伴隨函子,那麼這是不是「一一對應」呢?

上面已經回答了一大半了,剩下的問題是:我有一對伴隨函子,它們產生的 monad 再產生的 monad-algebra 的伴隨函子,和一開始的那個伴隨函子「一樣」嗎?當然了,要比較兩個範疇或者函子是不是「一樣」,總要給出函子或者自然變換才行。

這裡神奇的事情又出現了:從 到 有唯一的函子與已知的伴隨函子交換。從唯一性不難得出這個函子把乙個物件 送到 ,然後簡單驗證一下即可。

所以問題就變成了:這個 canonical 的函子是否是等價?

Remark.這個 也叫 Eilenberg-Moore category,還有另外乙個類似的 Kleisli category ,其萬有性質是從 到 有唯一的函子與伴隨函子交換。不過這裡似乎用不上,就不細說了。

當然這個函子不一定是等價了,如果是等價的話, 豈不意味著 monad 和伴隨函子「的確就是一樣的」,那為啥還要研究 monad 呢?(不過大概也不能直接這麼說)

所以按照慣例,對「好的」給個定義,然後去研究什麼時候是「好的」。

Definition.如果這個 canonical 的函子是等價,那麼一開始的伴隨函子稱為 monadic 的。

所以問題變成了:什麼樣的伴隨函子是 monadic 的呢?不過這只是把一開始的問題換了個說法,其實問題還在那裡沒變。

讓我們先去看另乙個(也出現在本問題描述中的)問題:為什麼說 monad 表達了「生成元和關係」?

用生成元和關係來表達乙個代數物件是一種常用的手段。比如要表達乙個群,並不需要把所有群元素和乘法表給寫出來,這樣太麻煩了;一種辦法是給出其中某些元素(生成元)和它們之間的乘法等式(關係)。舉個例子:

對於二面體群 ,只需要找到兩個元素 (旋轉 )和 (相對於某一固定軸線的映象對稱),那麼所有群元素都是它們的乘積;這兩個元素滿足關係 ,且這樣的描述唯一(同構地)確定了這個群。比如代數拓撲一開始就會計算某拓撲空間的基本群,這種時候要描述算出來的群基本上只能這麼描述;對於拓撲空間的上同調環也是類似的。這樣的描述方法也出現在阿貝爾群、模或者別的地方。

我們把上面的說法用更 categorical 的語言來表述一下:對每個群 ,可以把它寫成某個自由群 的商,即有滿射 ;只要我們知道其 kernel 當然就能決定 了,或者更一般地,得到某一正合列 ,開頭的對映並不必須是單射。類似的在模論中能看到乙個模的 (free) presentation。

當然在一般的範疇裡面不一定有零物件,所以不應該說 (co)kernel 而應該說 (co)equalizer。所謂「monad 表達了生成元和關係」,就是說這裡有一種 canonical 的「生成元-關係」表達。具體來說:

Proposition.如果 是 上的乙個 monad 而 是乙個 -algebra,那麼有 中的 coequalizer 。這裡的雙箭頭是兩個態射 ,而右邊的態射是 。

這裡直接驗證也可以,而另一種辦法是這樣的:首先在 的作用下把這個 coequalizer 打到 裡面,會發現這能延拓成乙個 split coequalizer,那麼只需要說明 這個函子具有某種特別(複雜)的性質即可——粗略來說就是能把 中的某種 split coequalizer 拉回到 中的 coequalizer。

Definition.乙個函子 能夠 create coequalizers of -split pairs 的意思是:如果有 中的一對態射 且在 中能夠把 延拓為 split coequalizer,那麼能在 中將其延拓為 coequalizer,且用 打過來同構於給定的 coequalizer;此外所有在 中打過來是指定的 coequalizer 的圖都一定是 coequalizer。

這個事情我說得很複雜,所以建議大家都去看看書或者維基百科或者 nLab,畢竟我在這裡十分彆扭地說幾句很難說明白。

Theorem.一對伴隨函子 是 monadic 的當且僅當 creates coequalizers of -split pairs。

這個定理就終於回答了上一節的問題。

到這裡其實原先的問題已經很明確了:給定範疇 ,其上所有 monad 的範疇 到 有自然的遺忘函子 ,其左伴隨函子 (如果存在)則被稱為 free-monad 函子;自然地,這一對伴隨函子給出的 monad 就稱為 free-monad monad;於是這個 monad 對應的 monad-algebra 就稱為 free-monad monad monad-algebra。

原命題說 free-monad monad monad-algebra 就是 monad,這就是在說遺忘函子 是 monadic 的。怎麼證明呢?當然是用上一節的定理了(雖然我沒有說怎麼證明)。

我們來說個更一般的命題:

Proposition.設 是乙個 monoidal category,其上所有 monoid(或者叫 algebra,不要與 monad-algebra 相混淆)構成範疇 ,如果自然的遺忘函子 有左伴隨函子,則它是 monadic 的。

這當然能推出上面的命題了。作為特例,集合範疇 和其上的 Cartesian product 構成了 monoidal category,而 就是么半群的範疇。其實只要看過集合-么半群的 monadicity 證明,一般的 monoidal category 這裡的證明也是一樣的。

我們簡單說一下這個證明。首先要明確究竟要證什麼,因為那個定理和定義顯得有點複雜。假定有兩個在 中的態射 ,且在 中有 split coequalizer ,我們需要證明的是:

能夠在 上給出乙個 algebra 的結構

使得 是 algebra morphism

在 中 是 coequalizer

實際上給出第一點之後,後面兩條就比較容易驗證了。首先 unit 當然是由復合對映 給出的。為了給出乘法 ,注意到任何函子都保持 split coequalizer,所以有 coequalizer ;因為 都是 algebra,所以乘法就給出了前兩者向 的態射;接下來由 coequalizer 的萬有性質就給出了 的態射。

為了驗證所有的 algebra 的公理,只需要從 是 algebra 的公理出發畫交換圖,並注意到 coequalizer 是 epimorphism 即可。

當然說了這麼多,其實不自己操作一番大概也不知道我說錯了沒。範疇論的證明大抵如此,不自己去畫畫圖或者看人追一下圖,還是很難理解證明本身的。

不過這裡還遺留了乙個問題:函子 的左伴隨存在嗎?這個似乎也不大一定,還是得看具體的範疇來決定。(到現在我還是不太會判斷乙個函子的伴隨函子是否存在)

順帶可以說一說另乙個構造:如果在 monoidal category 中存在 coproduct 並且張量積保持 coproduct,那麼可以定義 ,加上適當的自然變換得到乙個 monad。顯然自由么半群或者張量代數都是這麼構造的。

如何理解 TCP IP, SPDY, WebSocket 三者之間的關係?

龍騰道默默地 TCP是基於IP IP是一種協議,不是IP位址 實現的,HTTP 1.1 SPDY WebSocket HTTP2.0是基於TCP實現的。IP 乙個底層網路定址協議。TCP 乙個相對可靠確保資訊送達 且按順序送達的中層資訊傳輸協議,效能相對於UDP較差。HTTP 1.1 上層網頁資訊傳...

如何理解functional programming裡的currying與partial application

李欣宜 定義乙個多參函式f arg1,arg2 argn 時,如果每個引數argi的型別為ti,這個多參函式最後的返回結果的型別為rtype,那麼可以說f的型別為 t1 t2 tn rtype 這是很多語言對於多參函式的解釋,把這些引數作為乙個tuple或者list傳入,即 t1 t2 tn 型別的...

如何理解 It make A one of Canada s most popular cities to live in ?

加拿大公共健康 這個語法有問題。It makes.A stands for a city s name. 首先,絕對是It makes.然後,回答題主的問題 1 正解 2 最高端要求有範圍的限定,所以平時一般看到的最高端都加定冠詞。但是Canada s已經是個範圍的限定,就不需要了,再舉幾個例子 o...