是否有一個monad沒有相應的monad變換器（IO除外）？

Question

到目前爲止，我遇到的每個monad（可以表示爲一種數據類型）都有一個對應的monad變換器，或者可以有一個。有沒有這樣的monad？或做所有單子有一個相應的變壓器？

相當於單子m我的意思是t Identity同構於m一個變壓器t。當然，它符合monad變壓器法律，並且t n是任何monad n的monad。

我希望看到一個證明（理想情況下是建設性的），即每個monad都有一個，或者某個特定monad的例子（沒有證明）。我對哈斯克爾導向的更多答案以及（類別）理論答案都感興趣。

作爲一個後續問題，是否有一個單子m有兩個不同的變壓器t1和t2？即，t1 Identity與t2 Identity同構並且與m同構，但是存在單調n，使得t1 n不同構於t2 n。

（IO和ST有一個特殊的語義，所以我不考慮它們在這裏，讓我們完全不理會他們。我們只專注於可使用的數據類型來構建「純粹」的單子。）

Answer 1

這裏的一個手形波浪我不太確定的答案。

Monads可以被認爲是命令式語言的接口。 return是如何爲語言注入純粹的價值，而>>=是如何將語言片斷拼接在一起的。 Monad法則確保語言的「重構」部分以您期望的方式工作。 monad提供的任何其他操作都可以被認爲是它的「操作」。

Monad變形金剛是解決「可擴展效應」問題的一種方法。如果我們有一個Monad Transformer t，它轉換Monad m，那麼我們可以說語言m正在擴展，可通過t獲得更多操作。 Identity monad是沒有效果/操作的語言，因此將t應用於Identity只會爲您提供一種語言，僅使用t提供的操作。因此，如果我們根據「注入，拼接和其他操作」模型考慮Monad，那麼我們可以使用Free Monad Transformer重新配置它們。即使是IO monad也可以這樣變成變壓器。唯一的解決方法是，你可能需要某種方法在某一時刻將該層從變壓器堆棧上剝離下來，而唯一明智的方法是在堆棧底部有IO，以便您可以在那裏執行操作。

Answer 2

我與@Rhymoid在這一個，我相信所有Monad有兩個（!!）變壓器。我的構造有點不同，而且不太完整。我希望能夠將這幅素描作爲一個證明，但我認爲我要麼缺少技能/直覺，要麼可能會涉及很多。

由於Kelisli，每單子（m）可以被分解爲兩個函子F_k和G_k使得F_k留伴隨於G_k和m是同構的G_k * F_k（這裏*是函子組合物）。另外，由於附件，F_k * G_k形成一個共同的。

我聲稱t_mk定義爲使得t_mk n = G_k * n * F_k是單子變壓器。顯然，t_mk Id = G_k * Id * F_k = G_k * F_k = m。對於這個算符定義return並不困難，因爲F_k是「尖」算符，並且限定join應該是可能的，因爲extract從comonad F_k * G_k可用於(t_mk n * t_mk n) a = (G_k * n * F_k * G_k * n * F_k) a類型的值減少到G_k * n * n * F_k型，然後將其進一步通過減少的值join從n。

因爲F_k和G_k不是Hask的內生工具，所以我們必須小心一點。所以，它們不是標準Functor類型類的實例，並且也不能直接與組合的n如上所示。相反，我們以「項目」 n到組成前Kleisli類，但我相信return從m規定「投影」。

我相信你也能做到這一點與Eilenberg摩爾定律單子分解，從而m = G_em * F_em，tm_em n = G_em * n * F_em，以及類似的結構爲lift，return，並join從comonad F_em * G_em上extract類似的依賴性。

Answer 3

我的解決方案利用了Haskell術語的邏輯結構。大家都知道，具有返回類型t的Haskell中的函數可以轉化爲具有返回類型（Monad m）=> m t的monadic函數。因此，如果「綁定」功能可以使其程序文本「monadified」適當，結果將是一個monad變換器。

的癥結是沒有理由的「綁定」操作的「monadification」應滿足法律，特別是關聯性。這是截斷消除的地方。截斷消除定理對內聯所有允許綁定，案例分析和應用程序的程序文本產生影響。而且，特定術語的所有計算最終都在一個地方執行。

由於「綁定」的類型參數是剛性的，「綁定」的右手側的用途可以通過返回值索引。這些術語最終位於返回結構中使「綁定」關聯的位置，因此右側的使用必須在「monadified」「綁定」中關聯，並且生成的結構是monad。

這實在是毛茸茸的，所以這裏是一個例子。請看下面的列表嚴格單子：

rseq x y = case x of x:xs -> (x:xs) : y [] -> [] : y

evalList (x:xs) = rseq x (evalList xs) evalList [] = []

instance Monad [] where return x = [x] ls >>= f = concat (evalList (map f ls))

評價此順序導致標準ListT（不是一個真正的單子）。然而，通過切割消除：

instance Monad [] where return x = [x] ls >>= f = case ls of [] -> [] x:xs -> case f x of y:ys -> (y:ys) ++ (xs >>= f) [] -> [] ++ (xs >>= f)

這提供了準確的評估，以進行 「monadified。」

---

響應於彼得Pudlak：

如果有問題的單子的類型是一些功能類型（方便的是教會編碼的所有數據類型），則該函數類型是由裝飾轉換所有返回的類型與轉換後的monad值。這是monadification的類型部分。 monadification的價值部分使用「return」提升純粹的功能，並使用「綁定」將它們與monad類型的居民的使用結合起來，從而保留了原始程序文本的評估順序。

嚴格列表單子被給出作爲評價順序不相關聯地構成，由該ListT使用相同的評價順序的嚴格列表單子的事實作爲見證的一個例子。

爲了完成這個例子，列表單子教會編碼是：

data List a = List (forall b. b -> (a -> List a -> b) -> b)

Monadified，就變成：

data ListT m a = ListT (forall b. m b -> (a -> List a -> m b) -> m b)

cons x xs = \_ f -> f x xs

nil = \x _ -> x

instance (Monad m) => Monad (ListT m) where return x = cons x nil ls >>= f = ls nil (\x xs -> f x >>= \g -> g (liftM (nil ++) (xs >>= f)) (\y ys -> liftM (cons y ys ++) (xs >>= f))

爲了詳細說明上述情況，切步消力數值全部使用堆棧紀律，確保在結構結果的順序評估順序一致消耗 - 這是以潛在的價格多次運行相同的動作。 [技術上，你需要的是切除近似值：A是B的切除消除（近似值），如果對於B的每個有限近似值，存在A的有限近似值，使得A是切消除B.]

我希望有所幫助。