我正忙于閱讀 Bartosz Milewski 為程式員撰寫的類別理論書，并且在將幺半群描述為一個集合和將幺半群描述為一個類別之間移動時，我正在努力描述非恒等態射。
我知道當在一個集合的背景關系中查看一個幺半群（例如一個字串）時，我們有興趣描述利用“附加”特征的各種函式，例如一個附加“狗”的函式或一個函式將“mmm”附加到它收到的任何輸入。這些函式將分別將它們的輸入映射到字串集中的另一個元素。這顯然包括不附加任何內容的可能性。
當我們在一個類別的背景關系中查看這個幺半群時，據我所知，我們正在縮小到一個抽象級別，這個幺半群物件代表整個“字串”型別，我們不再對元素的映射方式感興趣在這種型別中相互關聯，因為我們將整個型別表示為單個點/物件。
在此之后，我假設在這個抽象級別上，在“Set”背景關系中描述的所有函式看起來都是相同的，因為它們都映射字串 -> 字串。在我看來，這意味著在類別的背景關系中，標識函式（不附加任何內容）看起來與前面提到的 AppendDog 或 AppendMmm 函式或任何其他函式相同。
不過，我的推理顯然是不正確的，正如書中的這張圖，從幺半群物件到自身的態射顯示為唯一物體：
作為結束語/總結：我不明白為什么一旦我們將其抽象為一個類別，我們仍然對描述幺半群集合中的函式感興趣。一旦集合成為一個類別中的物件，其中該物件代表整個型別，那么該集合中的所有函式是否看起來都不像恒等函式，從我們的新優勢來看，它們似乎都從該型別開始并回傳到該型別型別。
我希望我已經把我的困惑說清楚了。提前感謝您的幫助！
uj5u.com熱心網友回復：
我相信您正在觀察的是每個幺半群都與平凡的幺半群同態。如果你只看任何幺半群的點箭頭圖，它也是平凡幺半群的有效圖，但這張圖并不是全部。
當您“抽象”時，您實際上是在丟棄幺半群上的等價關系并補充可能的最弱的等價關系。Append"mm"和 Append"" 是不同的，但該圖并未說明這一點。可以想象它們是相等的，你會得到一個有效的幺半群，但這會改變等價關系。
即使我們丟棄了一些細節，也不應該丟棄它們不相等（或至少可能不相等）的事實。這對結構很重要。
uj5u.com熱心網友回復：
也許一個具體的例子會使這更容易討論。所以這是我的具體例子：
t
┌────┐
│ ▼
└─── ? ?──┐
│ │
└────┘
f
這是一個具有一個物件 ( ?) 和兩個態射 (t和f) 的范疇。這是一個完整的類別定義嗎？不，我們需要另一件事，即組合的定義。我會把它作為一個查找表。
f ° f = f
f ° t = t
t ° f = t
t ° t = f
這是一個完整的類別定義嗎？不，我們還需要一件事，那就是我們需要為每個物件識別一個態射作為恒等式。對于這個類別，只有一個物件，并且f具有該物件的正確行為。
這是一個完整的類別定義嗎？是的！您可能想驗證類別定律——即f° x = x ° f= x和 ( x ° y ) ° z = x ° ( y ° z ) - 但也歡迎您相信我的話. （如果它有助于您對這些證明的直覺，您可能希望將其讀f作“假”、t“真”，將°讀作 XOR。）
好的，這是一個單一的物件類別。希望很清楚，并非所有的態射都是相同的。當然，真與假似乎是不同的概念！
現在將上面的類別定義與下面的幺半群定義進行比較。要定義一個幺半群，我們必須給出一個集合的三元組 (M, , 0)、一個二元運算和一個恒等式。定義：
M = {f, t}
f f = f
f t = t
t f = t
t t = f
0 = f
這指定 xor 下的布林值的幺半群。請注意我們的兩個發展是多么相似。對于類別，我們給出了一個點和箭頭圖，它標識了兩個箭頭f和t，而對于幺半群定義，我們給出了一個包含兩個元素的集合，f和t。對于范疇，我們給出了一個組合算子，它將兩個態射組合成一個，而對于幺半群，我們給出了一個取集合中的兩個元素并回傳一個元素的算子。對于類別，我們確定f為恒等態射，而對于幺半群，我們確定f為恒等元。對于類別，我們證明了 ° 是關聯的，而對于幺半群，我們證明了 是關聯的。對于類別，我們證明了與f什么都不做，而對于幺半群，我們證明了加到f什么都不做。
我們需要提供來定義一個幺半群的資料和我們需要提供來定義一個單物件類別的資料是相同的！
轉載請註明出處，本文鏈接：https://www.uj5u.com/ruanti/495430.html
上一篇：哈斯克爾警告