haskell - 预组合单子(monad)更改器(mutator)

Question

假设我有两个单子(monad)变压器

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 s 作用于一些 monad 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)转换器在应用于单子(monad)时可以产生一个非单子(monad)吗？如果没有，我应该能够摆脱 MonadTrans (X t1 t2) 的实例.

是否有一个技巧让我无法做到，或者是否有原因无法做到(理论上或当前编译器支持的限制)。

暗示是否对应于除

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

哪些会与其他实例重叠/无法提供特定绑定(bind)？这不能通过一些间接来解决吗？制作 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

由于重叠，这种实例目前无效，但是它们是否可行、有用？

Answer 1

[C]an a valid monad transformer produce a non-monad when applied to a monad?

不，monad 转换器是类型构造函数 t :: (* -> *) -> (* -> *)它将一个 monad 作为参数并产生一个新的 monad。

虽然我希望看到更明确的说明， the transformers documentation确实说“单子(monad)转换器从现有单子(monad)中生成新单子(monad)”， the MonadTrans laws 暗示了这一点:

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

显然，这些法律只有在 lift m 时才有意义。确实是一元计算。正如您在评论中指出的那样，如果我们有不合法的情况要处理，所有的赌注都将被取消。这是 Haskell，而不是 Idris，所以我们习惯于礼貌地要求使用文档来满足法律，而不是使用类型强制要求它。

更“现代”的 MonadTrans可能需要明确证明 t m每当 m 时都是单子(monad)是。这里我使用 the "entailment" operator :- 来自 Kmett's constraints library要说 Monad m暗示 Monad (t m) :

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

(这或多或少与@MigMit 在他的回答中提出的想法相同，但使用了现成的组件。)

为什么 MonadTrans 不在 transformers特色 transform成员？编写时 GHC 不支持 :-运算符( ConstraintKinds 扩展尚未发明)。世界上有很多代码依赖于 MonadTrans没有 transform ，所以如果没有 a really good reason，我们就无法真正返回并添加它，在实践中 transform方法并没有真正让你买多少。