在One Monad to Prove Them All的第 12 頁上，寫到“ [容器] 的一個突出示例是串列資料型別。串列可以由串列的長度和串列中映射位置的函式表示”。
起初我認為這個容器上的自由 monad 將與 list monad 同構。
但是在第 12 頁上，寫到“串列 monad 不是自由 monad，因為串列 monad 與自由 monad 的實體不同構”。
那么上面容器上的 free monad 是什么？它與什么同構？為什么它不與串列單子同構？它可以通過商同構嗎？
uj5u.com熱心網友回復：
我認為應該小心一點。
我不認為如果M是一個自由單子，那么應用自由單子結構會讓你回到與M. 所以你的“什么是自由單子X”的問題實際上與“什么函子是X自由單子的？”無關。為了證明 monadM不是一個自由的 monad，我們唯一需要做的就是展示一些M對 monad 法則來說是正確但不暗示的等式——因為自由 monad 構造的含義是它保證了 monad 法則而不是什么別的。
這是對串列執行此操作的一種方法：
f False = ""
f True = "x"
g False = "x"
g True = ""
is = [False, True]
現在is >>= f= is >>= g(= "x") 即使f!= g。
一個單獨的問題是通過將自由構造應用于串列得到什么 monad。作為一種直覺，考慮自由 monad 構造的一種方式是，它是它所轉換的東西的任意（和異構）深度嵌套版本。對于串列，這意味著像
[[[0], [1, [2, 3], 4]], [5,6,7]]
將是自由建設的成員。如果您稍微考慮一下，您會發現另一種思考方式是將其視為一棵樹，其葉子（僅）具有資料，并且每個內部節點都允許有任意數量的子節點。
只是為了好玩，我們可以仔細檢查一下我們沒有驗證之前的相等性。這次我們得到
is >>= f = ["", "x"]
is >>= g = ["x", ""]
所以我們可以走了。
轉載請註明出處，本文鏈接：https://www.uj5u.com/houduan/434063.html