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

问题描述

到目前为止，我遇到的每个 monad(可以表示为数据类型)都有一个相应的 monad 转换器，或者可以有一个.有没有这样的 monad 不能有一个?或者是否所有的 monad 都有相应的转换器?

通过一个 transformer t 对应于 monad m 我的意思是 t Identity 与 同构米.当然，它满足 monad 转换器定律，并且 t n 是任何 monad n 的 monad.

我希望看到每个 monad 都有一个的证明(最好是构造性的)，或者是一个没有一个的特定 monad 的例子(有证明).我对更面向 Haskell 的答案以及(类别)理论答案都感兴趣.

作为后续问题，是否有一个具有两个不同转换器 t1 和 t2 的单子 m?也就是说，t1 Identity 与 t2 Identity 和 m 同构，但是有一个 monad n 使得t1 n 与 t2 n 不是同构的.

(IO 和 ST 有一个特殊的语义，所以我在这里不考虑它们，让我们完全忽略它们.让我们只关注纯"monads可以使用数据类型构造.)

解决方案

我和 @Rhymoid 一起讨论这个问题，我相信所有 Monad 都有两个 (!!) 转换器.我的构建有点不同，而且远不完整.我希望能够将这个草图用于证明，但我认为我要么缺少技能/直觉和/或它可能非常复杂.

由于 Kleisli，每个 monad (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 是一个 monad 转换器.显然，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 类型的值，然后通过 n 的 join 进一步减少.

我们必须小心一点，因为 F_k 和 G_k 不是 Hask 上的内函子.因此，它们不是标准 Functor 类型类的实例，也不能直接与 n 组合，如上所示.相反，我们必须在组合之前将 n投影"到 Kleisli 类别中，但我相信 m 的 return 提供了投影".>

我相信你也可以用 Eilenberg-Moore monad 分解来做到这一点，给出 m = G_em * F_em、tm_em n = G_em * n * F_em 和类似的lift、return 和 join 的结构与来自 comonad F_em 的 extract 类似的依赖 *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屋！