有没有一个monad没有相应的monad变压器（IO除外）？
到目前为止，我所遇到的每个monad（可以表示为一个数据types）都有一个对应的monad变换器，或者可以有一个。 有没有这样的monad？ 还是所有的monad都有相应的变压器？
通过对应于monad m的变换器t ，我的意思是t Identity同构同构于m 。 当然，它符合monad变压器法则，而且对于任何monad n来说都是monad。
我希望看到一个certificate（理想上是有build设性的），即每一个单子都有一个certificate，或者是一个没有certificate的单子的certificate。 我对哈斯克尔导向的答案以及（类别）理论答案都感兴趣。
作为一个后续的问题，是否有一个monad m有两个不同的变换器t1和t2 ？ 也就是说， t1 Identity同构于t2 Identity和m ，但是有一个monad n使得t1 n不同构于t2 n 。
（ IO和ST有一个特殊的语义，所以我不考虑它们，让我们完全忽略它们，让我们只关注可以使用数据types构造的“纯”单子。
我和@Rhymoid在这一个，我相信所有Monad有两个（!!）变压器。 我的build设有点不同，而且不太完整。 我希望能够把这个素描作为一个certificate，但我想我要么缺less技能/直觉，要么可能会涉及到这个问题。
由于Kelisli，每个monad（ m ）可以分解成两个函子F_k和G_k ，使得F_k和G_k F_k被保留，并且m同构于G_k * F_k （这里*是函子的构成）。 另外，由于这个F_k * G_k ， F_k * G_k形成一个共同的。
我声称t_mk被定义为使得t_mk n = G_k * n * F_k是一个monad变换器。 显然， t_mk Id = G_k * Id * F_k = G_k * F_k = m 。 定义这个函子的return并不困难，因为F_k是一个“尖”的函数，定义join应该是可能的，因为从共同子F_k * G_k可以用来减lesstypes的值(t_mk n * t_mk n) a = (G_k * n * F_k * G_k * n * F_k) a到typesG_k * n * n * F_k ，然后通过n join进一步减less。
我们必须要小心一点，因为F_k和G_k并不是Hask的内生函数。 因此，它们不是标准Functortypes类的实例，也不能直接与n组合，如上所示。 相反，我们必须在构图之前将“投射”到Kleisli类别中，但是我相信从m return提供了“投影”。
我相信你也可以通过Eilenberg-Moore monad分解来完成这个任务，给出m = G_em * F_em ， tm_em n = G_em * n * F_em和类似的lift ， return和join的结构， F_em * G_em 。
这是一个手工波浪我不太确定的答案。
Monads可以被认为是命令式语言的接口。 return是你如何为语言注入一个纯粹的价值，而>>=是如何拼凑在一起的语言块。 Monad法则确保语言的“重构”部分按照您期望的方式工作。 monad提供的任何其他操作都可以被认为是它的“操作”。
Monad变形金刚是解决“可扩展效应”问题的一种方法。 如果我们有一个Monad Transformer t来转换一个Monad m ，那么我们可以说， 语言 m正在扩展，并且通过t可以获得额外的操作。 Identity monad是没有任何效果/操作的语言，因此将t应用于Identity只会为您提供一种只有t提供的操作的语言。
所以，如果我们从“注入，拼接和其他操作”的angular度来思考Monad，那么我们可以用Free Monad Transformer来重新构造他们。 即使是IO monad也可以这样变成变压器。 唯一的问题是，你可能需要某种方式来剥离变压器堆栈上的某一层，唯一合理的方法就是如果你在堆栈底部有IO ，那么你可以在那里执行操作。
我的解决scheme利用了Haskell术语的逻辑结构。 大家都知道，返回types为t的Haskell中的函数可以转化为返回types（Monad m）=> m t的monadic函数。 因此，如果“绑定”function可以使其程序文本“monadified”适当，结果将是monad变压器。
关键在于“绑定”运算符的“monadification”应该满足规律，特别是关联性，没有理由。 这是截断消除的地方。截断消除定理对内联所有绑定，案例分析和应用程序的程序文本有影响。 另外，特定术语的所有计算最终都在一个地方执行。
由于“绑定”的types参数是严格的，因此“绑定”右侧的使用通过它们的返回值进行索引。 这些术语最终在返回的结构中使“绑定”相关联，因此右侧的使用必须在“monadified”“绑定”中联合使用，并且生成的结构是monad。
这真的很毛茸茸，所以这里就是一个例子。 考虑以下严格的monad列表：
rseq xy = 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（不是一个monad）。 但是，通过削减消除：
instance Monad [] where return x = [x] ls >>= f = case ls of [] -> [] x:xs -> case fx of y:ys -> (y:ys) ++ (xs >>= f) [] -> [] ++ (xs >>= f)
这就提供了准确的评估指令“monadified”。
为了回应Petr Pudlak：
如果所讨论的monad的types是某种函数types（对所有数据types进行Church编码很方便），则函数types通过装饰所有types的返回值来转换。 这是monadification的types部分。 monadification的价值部分使用“返回”提升纯粹的function，并使用“绑定”结合monadtypes的居民的使用，保留原始程序文本的评估顺序。
严格的列表monad是作为一个不关联组合的评估顺序的例子，正如ListT使用与严格列表monad相同的评估顺序一样。
为了完成这个例子，列表monad的教会编码是：
data List a = List (forall b. b -> (a -> List a -> b) -> b)
Monadified，它变成：
data ListT ma = ListT (forall b. mb -> (a -> List a -> mb) -> mb)
cons x xs = \_ f -> fx xs
nil = \x _ -> x
instance (Monad m) => Monad (ListT m) where return x = cons x nil ls >>= f = ls nil (\x xs -> fx >>= \g -> g (liftM (nil ++) (xs >>= f)) (\y ys -> liftM (cons y ys ++) (xs >>= f))
为了详细说明上述情况，删除步骤强制使用堆栈规则来消耗所有的值，以确保结构中的结果顺序与评估顺序相匹配 – 这是以多次潜在地执行相同操作的代价来实现的。
[从技术上讲，你需要的是切除近似值：A是B的切割消除（近似值），如果对于B的每一个有限近似，存在A的有限近似，使得A是B的切除消除。 ]
我希望有帮助。
