是否有monad没有相应的monad变压器(IO除外)？

Question

到目前为止,我遇到的每个monad(可以表示为数据类型)都有相应的monad变换器,或者可以有一个.有这样一个不能有一个单子吗？或者所有monad都有相应的变压器？

通过对应于monad的变换器t,m我的意思t Identity是同构的m.当然,它满足monad变压器法则,并且t n是任何monad的monad n.

我希望看到每个monad都有一个证明(理想情况下是建设性的证明),或者没有一个证明(带证明)的特定monad的例子.我对更多面向Haskell的答案以及(类别)理论答案感兴趣.

作为后续问题,是有一个单子m是有两个不同的变压器t1和t2？也就是说,t1 Identity同构t2 Identity和m,但有一个单子n这样t1 n是不是同构t2 n.

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

Answer 1

我和@Rhymoid在一起,我相信所有Monads都有两个(!!)变形金刚.我的构造有点不同,而且不太完整.我希望能够将这个草图变成一个证明,但我认为我要么缺少技能/直觉和/或它可能参与其中.

由于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为单子变压器.显然,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然后通过joinfrom 进一步减少n.

我们确实是因为有些谨慎F_k,并G_k没有对Hask endofunctors.因此,它们不是标准Functor类型类的实例,也不能直接与n上面所示组合.相反,我们以"项目" n为组成前Kleisli类,但我相信return从m提供"投影".

我相信你也可以使用Eilenberg摩尔定律单子分解做到这一点,给予m = G_em * F_em,tm_em n = G_em * n * F_em以及类似的结构lift,return以及join对类似的相关性extract从comonad F_em * G_em.

Answer 2

这是一个我不太确定的挥手答案。

Monad 可以被认为是命令式语言的接口。return就是如何将纯值注入到语言中，以及>>=如何将语言的各个部分拼接在一起。Monad 法则确保“重构”语言片段按照您期望的方式工作。单子提供的任何附加操作都可以被视为它的“操作”。

Monad Transformers 是解决“可扩展效应”问题的一种方法。如果我们有一个 Monad Transformert来转换 Monad m，那么我们可以说该语言 m正在通过 可用的附加操作进行扩展t。monadIdentity是一种没有效果/操作的语言，因此应用t到Identity只会让你获得一种仅具有由 提供的操作的语言t。

因此，如果我们从“注入、拼接和其他操作”模型的角度来考虑 Monad，那么我们可以使用 Free Monad Transformer 重新表述它们。甚至 IO monad 也可以通过这种方式变成一个变压器。唯一的问题是，您可能需要某种方法在某个时刻将该层从变压器堆栈上剥离，而唯一明智的方法是如果您位于IO堆栈的底部，以便您可以在那里执行操作。