组合Monad变换器

Question

假设我有两个单子变换器。

T1 :: (* -> *) -> * -> *
T2 :: (* -> *) -> * -> *

使用实例

instance MonadTrans T1
instance MonadTrans T2

以及一些

X :: (((* -> *) -> * -> *) -> ((* -> *) -> * -> *) -> * -> *)

例如

newtype X t1 t2 a b = X { x :: t1 (t2 a) b }

为此，我希望定义一些类似的东西。

instance (MonadTrans t1, MonadTrans t2) => MonadTrans (X t1 t2) where
    lift = X . lift . lift

那么我该如何使用lift将m a提升为X T1 T2 m a？

这里的问题似乎是lift作用于一些单子Monad m => m a，而我不能保证在中间步骤中产生它。但对我来说这很令人困惑。我正在提供一个lift实现，因此我可以假设我有Monad m => m a，所以我应用最右侧的lift并得到T1 m a，我对其一无所知，但是难道不应该暗示着T1 m是一个Monad吗？如果不是，为什么我不能简单地将其添加到我的实例约束中？

instance ( MonadTrans t1
         , MonadTrans t2
         , Monad (t2 m) ) => MonadTrans (X t1 t2) where ...

这也不起作用。我有一种直觉，认为上述内容是在说“是否应该存在t1，t2和m，使得...”，这对于证明X t1 t2是一个变换器（适用于任何/所有的Monad m）来说太弱了。但是对我来说仍然没有多大意义，有效的monad transformer是否能产生一个非monad，如果不能，我应该能够通过MonadTrans (X t1 t2)的实例获得成功。

有没有什么诀窍可以做到这一点，只是我无法理解，还是有一个理论限制或当前编译器支持的限制导致无法完成？

这个暗示是否对应于其他任何东西？

instance (MonadTrans t, Monad m) => Monad (t m) where
    return  = lift . return
    a >>= b = ... # no sensible generic implementation

如果这样会重叠其他实例或无法提供特定绑定，这不是可以通过一些间接方式解决吗？将 returnT :: Monad m => a -> t m a 和 bindT :: Monad m => t m a -> (a -> t m b) -> t m b 加入到 MonadTrans 中，这样就可以编写以下代码：

instance MonadTrans (StateT s) where
    lift = ...
    returnT = ...
    bindT = ...

...

instance (MonadTrans t, Monad m) => Monad (t m) where
    return  = returnT
    a >>= b = a `bindT` b

这种实例目前由于重叠而无效，但如果它们可行，会有用吗？

- jakubdaniel

Answer 1

“一个有效的单子变换器在应用于单子时，能否产生非单子？”

不行。单子变换器是一种类型构造器 t :: (* -> *) -> (* -> *) ，它以单子作为参数并生成一个新的单子。尽管我希望更明确地说明，transformers文档确实说“单子变换器从现有单子中创建新的单子”，而且这也被MonadTrans法则所暗示：

lift . return = return
lift (m >>= f) = lift m >>= (lift . f)

显然，这些法则只有在lift m确实是单子运算时才有意义。正如您在评论中指出的那样，如果我们需要处理非法例，则所有赌注都将无效。这是Haskell，而不是Idris，因此我们习惯于使用文档礼貌地要求满足法规，而不是使用类型强制要求它。

一个更“现代”的MonadTrans可能需要明确证明t m是一个单子，无论m是什么。这里我使用“蕴含”运算符:-从Kmett的constraints库中说Monad m意味着Monad (t m):

class MonadTrans t where
    transform :: Monad m :- Monad (t m)
    lift :: Monad m => m a -> t m a

这个想法与@MigMit在他的回答中开发的想法基本相同，但使用了现成的组件。

为什么transformers中的MonadTrans没有transform成员？当它被编写时，GHC不支持:-运算符（ConstraintKinds扩展还没有被发明）。世界上有很多很多依赖于没有transform的MonadTrans的代码，所以我们不能真正地回头添加它，除非有一个非常好的理由，而实际上transform方法并没有带来太多好处。

- Benjamin Hodgson

---

谢谢！有没有可能被添加进去？ - jakubdaniel

当你尝试使用transform进行一些有趣的操作时，例如将单子变换器堆栈作为一等公民，你需要每个你感兴趣的变换器都有一个可用的transform，而不仅仅是在transformers中的那些。如果某个变换器MyT具有transform = undefined，那么我就不能使用ReaderT r :.: MyT作为变换器，因为lift和>>=会崩溃。（transform包含实际有用的运行时数据，即（获取）>>=和return的实现方式。） - Benjamin Hodgson

我不明白lift如何依赖于transform，特别是在当前代码中它并没有这样做。 - jakubdaniel

@jd823592 我需要它告诉解释器将调用分派到 lift 的位置。 - Benjamin Hodgson

但是 transform 只在 transformers-0.5 中不可能出现的上下文中使用，那么为什么它会对所有代码都产生影响呢？抱歉我很蠢。 - jakubdaniel

Answer 2

首先：你想要的是不可能的。你已经正确地识别了问题：即使 m 是一个单子，t 是一个转换器，也没有人保证 t m 会成为一个单子。

另一方面，通常情况下它确实是的。但是-至少在理论上-并不总是如此，因此，您必须以某种方式标记它是的情况。这意味着用自己定义的另一个类型类的实例来标记它。让我们看看它是如何工作的。

我们将从为我们的新类命名开始：

class MonadTrans t => MonadTransComposeable t where

现在，我们要做什么呢？我们想要生成一个 Monad (t m) 实例。不幸的是，这不是我们能够完成的事情。尽管类实例只是数据，但它们与其他所有数据并不被认为是同一种类型的数据；我们无法创建一个生成它们的函数。因此，我们必须以某种方式解决这个问题。但是，如果我们有这样一个东西，那么这个类就非常简单了。

class MonadTrans t => MonadTransComposeable t where
    transformedInstance :: Monad m => MonadInstance (t m)

现在让我们定义MonadInstance。我们想要确保如果有MonadInstance n，那么n就是一个单子。 GADT可以帮助我们：

data MonadInstance n where MonadInstance :: Monad n => MonadInstance n

注意，MonadInstance构造函数有一个上下文，这保证了我们不能在没有n被Monad的情况下创建MonadInstance n。

现在我们可以定义MonadTransComposeable的实例：

instance MonadTransComposeable (StateT s) where
    transformedInstance = MonadInstance

由于已经在transformers包中确定了每当m是单子时，StateT m也是单子，因此MonadInstance构造函数是有意义的。

现在我们可以组合MonadTrans和MonadTransComposeable。使用您自己的定义。

newtype X t1 (t2 :: (* -> *) -> (* -> *)) m a = X { x :: t1 (t2 m) a }

我们可以定义一个实例。现在我们可以证明t2 m是一个单子；这并非自动完成，我们必须告诉Haskell要使用哪个transformedInstance，但这并不难：

instance (MonadTrans t1, MonadTransComposeable t2) => MonadTrans (X t1 t2) where
  lift :: forall m a. (Monad m) => m a -> X t1 t2 m a
  lift ma =
    case transformedInstance :: MonadInstance (t2 m) of
      MonadInstance -> X (lift (lift ma))

---

现在，让我们做些有趣的事情。 让我们告诉Haskell，只要t1和t2是“好的”（可组合的）单子变换器，X t1 t2也是如此。

与之前一样，这很容易：

instance (MonadTransComposeable t1, MonadTransComposeable t2) => MonadTransComposeable (X t1 t2) where
  transformedInstance = MonadInstance

和 StateT 一样。问题在于，现在 Haskell 会抱怨它不知道 X t1 t2 m 是否真的是一个 monad。这是公平的——我们没有定义一个实例。让我们来做这个。

我们将利用 t1 (t2 m) 是一个 monad 这个事实。因此，我们明确地表示出来：

transformedInstance2 :: forall t1 t2 m. (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => MonadInstance (t1 (t2 m))
transformedInstance2 =
  case transformedInstance :: MonadInstance (t2 m) of
    MonadInstance -> transformedInstance

现在，我们将定义一个 Monad (X t1 t2 m) 实例。由于让 Monad 成为 Applicative 的子类是一个愚蠢的决定，我们不能在一条语句中完成此操作，而必须通过 Functor 和 Applicative，但这并不难：

instance (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => Functor (X t1 t2 m) where
  fmap h (X ttm) =
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of
      MonadInstance -> X (fmap h ttm)

instance (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => Applicative (X t1 t2 m) where
  pure a =
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of
      MonadInstance -> X (pure a)
  (X ttf) <*> (X tta) =
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of
      MonadInstance -> X (ttf <*> tta)

而最后，

instance (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => Monad (X t1 t2 m) where
  X tta >>= f =
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of
      MonadInstance -> X (tta >>= \a -> case f a of X ttb -> ttb)

- MigMit

---

当你说并非每个转换后的单子都是一个单子时，你是指即使对于有意义的单子变换器，还是仅仅因为单子变换器的签名不能保证结果是一个单子（因为这是显而易见的，但通常还有其他规则适用于所有事物，所以这本身不是一个真正的问题）。如果将单子变换器应用于单子时产生虚假结果，那么为什么要称其为单子变换器呢 :) - jakubdaniel

我的意思是，“monad trans的签名不能保证结果是一个monad”。 - MigMit

要使其正常工作，需要一堆扩展。确切地说，需要 GADTs、ScopedTypeVariables、KindSignatures 和 InstanceSigs。 - MigMit

并不奇怪 (* -> *) -> * -> * 并不一定产生一个单子，从这个意义上说，甚至每个 Monad 都不是 Functor... 只有一个违反法律的虚假 Monad 也可以违反 Functor 法律... - jakubdaniel

Answer 3

有一个著名的理论认为单子不一定是可组合的。也就是说，对于任意两个任意的单子 t 和 u，不能保证 t ○ u 是一个单子，其中 (t ○ u) a = t (u a)。这似乎是为什么预组合不可用的根本原因。

理由很简单。首先，注意到任何单子都可以被写成恒等单子的变换。然后，任何两个单子都可以转化为 X 的形式。这对应于它们的组合，但通常不允许，所以我们知道通常不应该允许 X。

设 Id 为恒等单子。

newtype Id a = Id a

并且假设给定组成如下：

newtype t ○ u a = Comp (t (u a))

同时，对于任何单子 t，与 Id 的组合等于 t。

t ○ Id ~ t ~ Id ○ t

接下来，我们将调查 X t u m a 的情况，其中 t 和 u 是与 Id 组合的。类型和构造如下：

X (t ○) (Id ○ (u ○)) (Id ○ m) a 
  = X ((t ○) (Id ○ (u ○ (Id ○ m)) a)

而且RHS构造函数等同于

  ~ X ((t ○) (u ○ m) a)

它的类型是什么

X (t ○) (u ○) m a

因此，部分应用程序X（t○）（u○）对应于任何两个单子的组合，这是不允许的。

所有这些并不是说我们不能组合单子，而是解释为什么我们需要像Benjamin Hodgson和MigMit提供的transform或MonadTransComposable等方法。

我已经将这个设为社区wiki，因为我希望真正知道他们在做什么的人可以大大改进上述的松散证明。

- trevor cook