是否有一个monad没有相应的monad变换器（IO除外）？ [英] Is there a monad that doesn't have a corresponding monad transformer (except IO)?

问题描述

到目前为止，我遇到的每个monad（可以表示为一种数据类型）都有一个对应的monad变换器，或者可以有一个。有没有这样的monad？或所有monad都有相应的转换器吗？ 通过转换器 t 对应于monad m 我的意思是 t Identity 是同构于 m 。当然，它满足monad变压器法则，并且 tn 是任何monad n 的单子。

我希望看到一个证明（理想情况下是建设性的），即每个monad都有一个证明，或者一个没有证明monad的例子（带证明）。我对哈斯克尔导向的答案以及（类别）理论答案都感兴趣。

作为后续问题，是否有monad m 有两个不同的转换器 t1 和 t2 ？也就是说， t1 Identity 同构于 t2身份并且< m ，但是有一个monad n ，所以 t1 n 不是同构于 t2 n 。

（ IO 和 ST 有一个特殊的语义，所以我没有把它们考虑在内，让我们完全忽略它们，让我们只关注可以使用数据类型构造的纯monad。）

解决方案

我在@Rhymoid上，我相信所有Monad都有两个（!!）变形金刚。我的构造有点不同，而且不太完整。我希望能够将这个草图作为一个证明，但我认为我要么缺少技能/直觉，要么可能涉及到其他人。

由于Kleisli，每个monad（ m ）可以分解为两个函子 F_k 和 G_k 使得 F_k 与 G_k 相同，并且 m 同构于 G_k * F_k （这里 * 是仿函数的构成）。此外，由于附加条件， F_k * G_k 构成了一个comonad。 我声称 t_mk 定义为使得 t_mk n = G_k * n * F_k 是一个monad变换器。显然， t_mk Id = G_k * Id * F_k = G_k * F_k = m 。由于 F_k 是一个指向函数，定义 return 并不困难> join 应该是可能的，因为从 F_k * G_k 可以用 extract> 将类型（t_mk n * t_mk n）a =（G_k * n * F_k * G_k * n * F_k）a 的值减少为类型 G_k * n * n * F_k ，然后通过 n 从 join 。

自 F_k 和 G_k 不是Hask的内部工作者。因此，它们不是标准 Functor typeclass的实例，也不能直接与 n 组合，如上所示。相反，我们必须在合成之前将 n 投影到Kleisli类别中，但我相信 return 是从 m 提供了投影。

我相信你也可以用Eilenberg-Moore monad进行分解，给出 m = G_em * F_em ， tm_em n = G_em * n * F_em ，以及类似的结构 lift ， return 和加入，对 extract> / code>来自comonad F_em * G_em 。

So far, every monad (that can be represented as a data type) that I have encountered had a corresponding monad transformer, or could have one. Is there such a monad that can't have one? Or do all monads have a corresponding transformer?

By a transformer t corresponding to monad m I mean that t Identity is isomorphic to m. And of course that it satisfies the monad transformer laws and that t n is a monad for any monad n.

I'd like to see either a proof (ideally a constructive one) that every monad has one, or an example of a particular monad that doesn't have one (with a proof). I'm interested in both more Haskell-oriented answers, as well as (category) theoretical ones.

As a follow-up question, is there a monad m that has two distinct transformers t1 and t2? That is, t1 Identity is isomorphic to t2 Identity and to m, but there is a monad n such that t1 n is not isomorphic to t2 n.

(IO and ST have a special semantics so I don't take them into account here and let's disregard them completely. Let's focus only on "pure" monads that can be constructed using data types.)

解决方案

I'm with @Rhymoid on this one, I believe all Monads have two (!!) transformers. My construction is a bit different, and far less complete. I'd like to be able to take this sketch into a proof, but I think I'm either missing the skills/intuition and/or it may be quite involved.

Due to Kleisli, every monad (m) can be decomposed into two functors F_k and G_k such that F_k is left adjoint to G_k and that m is isomorphic to G_k * F_k (here * is functor composition). Also, because of the adjunction, F_k * G_k forms a comonad.

I claim that t_mk defined such that t_mk n = G_k * n * F_k is a monad transformer. Clearly, t_mk Id = G_k * Id * F_k = G_k * F_k = m. Defining return for this functor is not difficult since F_k is a "pointed" functor, and defining join should be possible since extract from the comonad F_k * G_k can be used to reduce values of type (t_mk n * t_mk n) a = (G_k * n * F_k * G_k * n * F_k) a to values of type G_k * n * n * F_k, which is then further reduces via join from n.

We do have to be a bit careful since F_k and G_k are not endofunctors on Hask. So, they are not instances of the standard Functor typeclass, and also are not directly composable with n as shown above. Instead we have to "project" n into the Kleisli category before composition, but I believe return from m provides that "projection".

I believe you can also do this with the Eilenberg-Moore monad decomposition, giving m = G_em * F_em, tm_em n = G_em * n * F_em, and similar constructions for lift, return, and join with a similar dependency on extract from the comonad F_em * G_em.

这篇关于是否有一个monad没有相应的monad变换器（IO除外）？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！