有没有对应的 monad 转换器（IO 除外）的 monad？

我和@Rhymoid 合作，我相信所有的 Monad 都有两个（！！）变压器。我的结构有点不同，而且远没有那么完整。我希望能够将此草图作为证明，但我认为我要么缺少技能/直觉和/或它可能非常复杂。

由于 Kleisli，每个 monad (m) 都可以分解为两个函子 F_k 和 G_k，使得 F_k 与 G_k 相邻并且 m 与 G_k * F_k 同构（这里 { 8} 是函子组合）。此外，由于附加，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 应该是可能的，因为来自comonad 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 类型的值，然后通过 join 从 n 进一步减少。

由于 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 的类似结构，并具有对 extract 的类似依赖关系共轭 F_em * G_em。

---

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

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

Monad Transformers 是解决“可扩展效果”问题的一种方法。如果我们有一个转换 Monad m 的 Monad Transformer t，那么我们可以说 语言 m 正在扩展，可通过 t 获得额外的操作。 Identity monad 是没有效果/操作的语言，因此将 t 应用于 Identity 只会让您获得一种只有 t 提供的操作的语言。

因此，如果我们根据“注入、拼接和其他操作”模型来考虑 Monad，那么我们可以使用 Free Monad Transformer 重新构造它们。甚至 IO monad 也可以通过这种方式变成一个转换器。唯一的问题是，您可能希望通过某种方式在某个时候将该层从变压器堆栈上剥离，而唯一明智的做法是在堆栈底部有 IO，这样您就可以执行那里的操作。

---

以前，我以为我找到了没有转换器的明确定义的 monad 的示例，但这些示例是不正确的。

Either a (z -> a) 的转换器是 m (Either a (z -> m a)，其中 m 是任意外部 monad。 (a -> n p) -> n a 的转换器是 (a -> t m p) -> t m a，其中 t m 是 monad n 的转换器。

自由指向的单子。

此示例的 monad 类型构造函数 L 定义为

  type L z a  = Either a (z -> a)

这个 monad 的目的是用显式的 pure 值 (Left x) 修饰普通的 reader monad z -> a。普通的 reader monad 的 pure 值是一个常量函数 pure x = _ -> x。但是，如果给定一个 z -> a 类型的值，我们将无法确定该值是否是一个常量函数。对于 L z a，pure 值明确表示为 Left x。用户现在可以在 L z a 上进行模式匹配，并确定给定的一元值是纯的还是有效果的。除此之外，monad L z 与 reader monad 的作用完全相同。

单子实例：

  instance Monad (L z) where
     return x = Left x
     (Left x) >>= f = f x
     (Right q) >>= f = Right(join merged) where
        join :: (z -> z -> r) -> z -> r
        join f x = f x x -- the standard `join` for Reader monad
        merged :: z -> z -> r
        merged = merge . f . q -- `f . q` is the `fmap` of the Reader monad
        merge :: Either a (z -> a) -> z -> a 
        merge (Left x) _ = x
        merge (Right p) z = p z

这个 monad L z 是一个更一般的结构的特殊情况，(Monad m) => Monad (L m) where L m a = Either a (m a)。此构造通过添加显式 pure 值 (Left x) 来修饰给定的 monad m，以便用户现在可以在 L m 上进行模式匹配以确定该值是否为纯值。在所有其他方面，L m 表示与单子 m 相同的计算效果。

L m 的 monad 实例与上面的示例几乎相同，只是需要使用 monad m 的 join 和 fmap，辅助函数 merge 定义为

    merge :: Either a (m a) -> m a
    merge (Left x) = return @m x
    merge (Right p) = p

我用任意单子 m 检查了单子定律是否适用于 L m。

这种构造在给定的 monad m 上给出了自由指向的函子。这种构造保证了单子上的自由指向函子也是单子。

自由指向的 monad 的转换器定义如下：

  type LT m n a = n (Either a (mT n a))

其中 mT 是 monad m 的 monad 转换器（需要知道）。

另一个例子：

type S a = (a -> Bool) -> Maybe a

这个单子出现在“搜索单子”here 的上下文中。 paper by Jules Hedges 还提到了搜索单子，更一般地说，“选择”单子的形式

 type Sq n q a = (a -> n q) -> n a

对于给定的 monad n 和固定类型 q。上面的搜索单子是具有 n a = Maybe a 和 q = () 的选择单子的特例。 Hedges 的论文声称（没有证据，但他后来使用 Coq 证明了）Sq 是 monad (a -> q) -> a 的 monad 转换器。

但是，monad (a -> q) -> a 有另一个“组合外部”类型的 monad 转换器 (m a -> q) -> m a。这与问题 Is this property of a functor stronger than a monad? 中探讨的“刚性”属性有关，即 (a -> q) -> a 是一个刚性单子，所有刚性单子都有“组合外部”类型的单子转换器。

通常，转换的 monad 本身不会自动拥有一个 monad 转换器。也就是说，一旦我们取一些外来的 monad m 并对其应用一些 monad 转换器 t，我们就得到一个新的 monad tm，而这个 monad 没有转换器：给定一个新的外来 monad n，我们不知道如何用 monad t m 变换 n。如果我们知道单子 m 的变换器 mT，我们可以先用 mT 变换 n，然后用 t 变换结果。但是，如果我们没有单子 m 的转换器，我们就会陷入困境：没有任何结构可以单独根据 t 的知识为单子 tm 创建转换器并适用于任意外来单子 m。

然而，在实践中，所有显式定义的 monad 都有显式定义的转换器，因此不会出现这个问题。

@JamesCandy 的回答表明，对于任何 monad（包括 IO？！），都可以编写一个（一般但复杂的）类型表达式来表示相应的 monad 转换器。也就是说，您首先需要对您的 monad 类型进行 Church-encode，这使得该类型看起来像一个 continuation monad，然后定义它的 monad 转换器，就像为 continuation monad 一样。但我认为这是不正确的——它没有给出一般生产单子变压器的配方。

采用类型 a 的 Church 编码意味着记下类型

 type ca = forall r. (a -> r) -> r

根据米田引理，这种类型 ca 与 a 完全同构。到目前为止，除了通过引入量化类型参数 forall r 使类型变得更加复杂之外，我们什么也没做。

现在让我们对一个基础 monad L 进行 Church 编码：

 type CL a = forall r. (L a -> r) -> r

同样，到目前为止我们什么也没做，因为 CL a 完全等同于 L a。

现在假设 CL a 是一个延续 monad（它不是！），并通过将结果类型 r 替换为 m r 来编写 monad 转换器，就好像它是一个延续 monad 转换器：

 type TCL m a = forall r. (L a -> m r) -> m r

这被称为 L 的“Church 编码的 monad 转换器”。但这似乎是不正确的。我们需要检查属性：

TCL m 是任何外来单子 m 和任何基本单子 L 的合法单子

ma -> TCL ma 是一个合法的一元态射

第二个属性成立，但我相信第一个属性失败，换句话说，TCL m 不是任意 monad m 的 monad。也许有些单子 m 承认这一点，但其他人不承认。我找不到对应于任意基本 monad L 的 TCL m 的通用 monad 实例。

另一种论证 TCL m 通常不是 monad 的方法是注意 forall r. (a -> m r) -> m r 确实是任何类型构造函数 m 的 monad。用 CM 表示这个 monad。现在，TCL m a = CM (L a)。如果 TCL m 是一个单子，则意味着 CM 可以与任何单子 L 组合并产生一个合法的单子 CM (L a)。然而，一个非平凡的单子 CM（特别是不等价于 Reader 的单子）不太可能与所有单子 L 组成。如果没有严格的进一步限制，Monad 通常不会组合。

这不起作用的一个具体示例是针对 reader monads。考虑 L a = r -> a 和 m a = s -> a，其中 r 和 s 是一些固定类型。现在，我们要考虑“Church 编码的单子变换器”forall t. (L a -> m t) -> m t。我们可以使用米田引理简化这个类型表达式，

 forall t. (x -> t) -> Q t  = Q x

（对于任何函子 Q）并获得

 forall t. (L a -> s -> t) -> s -> t
 = forall t. ((L a, s) -> t) -> s -> t
 = s -> (L a, s)
 = s -> (r -> a, s)

所以这是本例中 TCL m a 的类型表达式。如果 TCL 是一个 monad 转换器，那么 P a = s -> (r -> a, s) 就是一个 monad。但是可以明确地检查这个 P 实际上不是一个 monad（不能实现满足法律的 return 和 bind）。

即使这有效（即假设我在声称 TCL m 通常不是 monad 时犯了一个错误），这种结构也有某些缺点：

它对于外来的 monad m 不是函数的（即不是协变的），所以我们不能做一些事情，比如将一个转换后的自由 monad 解释为另一个 monad，或者合并两个 monad 转换器，如这里解释的那样有组合两个 monad 转换器的原则方法吗如果它们是不同的类型，但它们的底层 monad 是相同的类型？

forall r 的存在使该类型的推理变得非常复杂，并可能导致性能下降（请参阅“Church 编码被认为有害”论文）和堆栈溢出（因为 Church 编码通常不是堆栈安全的）

身份基单子 (L = Id) 的 Church 编码单子转换器不会产生未修改的外来单子：T ma = forall r。 (a -> mr) -> mr 这与 m a 不同。事实上，给定一个 monad m，很难弄清楚那个 monad 是什么。

作为说明为什么 forall r 使推理变得复杂的示例，请考虑外来单子 m a = Maybe a 并尝试理解类型 forall r. (a -> Maybe r) -> Maybe r 的实际含义。我无法简化这种类型或找到关于这种类型的作用的一个很好的解释，即它代表什么样的“效果”（因为它是一个单子，它必须代表某种“效果”）以及如何使用这样的类型。

Church-encoded monad 转换器不等同于标准的知名 monad 转换器，例如 ReaderT、WriterT、EitherT、StateT 等。

目前尚不清楚还有多少其他单子变压器存在，以及在什么情况下会使用一个或另一个变压器。

帖子中的一个问题是找到一个具有两个转换器 t1 和 t2 的 monad m 的显式示例，这样对于某些外来的 monad n，monad t1 n 和 t2 n 是不等价的。

我相信 Search monad 提供了这样一个例子。

 type Search a = (a -> p) -> a

其中 p 是固定类型。

变压器是

 type SearchT1 n a = (a -> n p) -> n a
 type SearchT2 n a = (n a -> p) -> n a

我检查了 SearchT1 n 和 SearchT2 n 是否都是任何单子 n 的合法单子。我们有提升 n a -> SearchT1 n a 和 n a -> SearchT2 n a，它们通过返回常量函数来工作（只返回给定的 n a，忽略参数）。我们有 SearchT1 Identity 和 SearchT2 Identity 显然等价于 Search。

SearchT1 和 SearchT2 之间的最大区别在于 SearchT1 在 n 中不是函数式的，而 SearchT2 是。这可能对“运行”（“解释”）转换后的 monad 有影响，因为通常我们希望能够将解释器 n a -> n' a 提升为“运行器”SearchT n a -> SearchT n' a。这可能仅适用于 SearchT2。

类似的缺陷存在于标准单子转换器中，用于延续单子和共密度单子：它们在外来单子中不是功能性的。

---

我的解决方案利用了 Haskell 术语等的逻辑结构。

我将右 Kan 扩展视为 monad 转换器的可能表示。众所周知，右 Kan 扩展是限制，因此它们应该作为任何感兴趣对象的通用编码是有道理的。对于单子函子 F 和 M，我查看了 MF 沿 F 的右 Kan 扩展。

首先，我证明了一个引理，“滚动引理”：右 kan 扩展的提议函子可以在其中滚动，给出任何函子 F、G 和 H 的映射 F(Ran GH) -> Ran G(FH)。

使用这个引理，我计算了右 Kan 扩展 Ran F (MF) 的一元连接，需要分配律 FM -> MF。如下：

Ran F(MF) . Ran F(MF) [rolling lemma] =>
  Ran F(Ran F(MF)MF) [insert eta] =>
  Ran F(Ran F(MF)FMF) [gran] =>
  Ran F(MFMF) [apply distributive law] =>
  Ran F(MMFF) [join Ms and Fs] =>
  Ran F(MF).

这种结构的有趣之处在于它允许函子 F 和 M 的提升如下：

(1) F [lift into codensity monad] =>
  Ran F F [procompose with eta] =>
  Ran F(MF).

(2) M [Yoneda lemma specialized upon F-] =>
  Ran F(MF).

我还调查了右 Kan 扩展 Ran F(FM)。在不诉诸分配律的情况下实现一元性似乎表现得更好一些，但在它提升的函子方面更加挑剔。我确定它会在以下条件下提升一元函子：

1) F 是一元的。

2) F |- U，在这种情况下它承认升力 F ~> Ran U(UM)。这可以在状态单子的上下文中用于“设置”状态。

3) M 在某些条件下，例如当 M 承认分配律时。

---