haskell - 是否有一个 monad 没有相应的 monad 转换器(IO 除外)？

Question

到目前为止，我遇到的每个 monad(可以表示为一种数据类型)都有一个相应的 monad 转换器，或者可以有一个。是否存在这样一个不可拥有的单子(monad)？或者所有单子(monad)都有相应的转换器吗？

通过变压器 t对应monad m 我的意思是t Identity同构于 m 。当然，它满足单子(monad)变换定律并且 t n是任何 monad 的 monad n .

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

作为后续问题，是否有一个 monad m有两个不同的变压器 t1和t2 ？即t1 Identity同构于 t2 Identity并发送至m ，但是有一个单子(monad) n这样t1 n与 t2 n 不同构.

( IO 和 ST 有特殊的语义，所以我在这里不考虑它们，让我们完全忽略它们。让我们只关注可以使用数据类型构造的“纯”单子(monad)。)

Answer 1

我在这个问题上支持 @Rhymoid，我相信所有 Monad 都有两个 (!!) 变压器。我的构建有点不同，而且远不完整。我希望能够将这个草图作为证明，但我认为我要么缺乏技能/直觉，要么它可能非常复杂。

由于 Kleisli，每个单子(monad) (m) 都可以分解为两个仿函数 F_k 和 G_k，这样 F_k code> 与 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 中的/code> 可用于减少 (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 from m 提供了这种“投影”。

我相信您也可以通过 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。