预制monad变压器

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对某些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

哪个会与其他实例重叠/无法提供特定的绑定？不能用一些间接来解决这个问题吗？制作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]一个有效的 monad 转换器在应用于 monad 时会产生非 monad 吗？

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

虽然我希望看到更明确的说明，但文档确实transformers说“单子转换器从现有的单子中生成新的单子”，并且法律暗示了这MonadTrans一点：

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

lift m显然，这些定律只有在确实是一元计算时才有意义。正如您在评论中指出的那样，如果我们有非法实例需要应对，那么所有的赌注都会被取消。这是 Haskell，而不是 Idris，因此我们习惯于使用文档礼貌地请求满足法律要求，而不是使用类型强制要求满足法律要求。

更“现代”的MonadTrans可能需要明确的证明，t m无论何时都是一个单子m。在这里，我使用Kmett库中的“蕴含”运算符:-来表示：constraintsMonad mMonad (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扩展尚未发明）。世界上有很多很多代码都依赖于 without MonadTrans，transform所以我们不能在没有充分理由的情况下真正回去添加它，而且在实践中，这种transform方法并没有给你带来太多好处。