为什么 `hoist` 函数会限制这个 monad 的类型参数？

Question

我有一个函数，可以组合两个单子：

comp :: Monad m => m a -> m b -> m b

我会帮助翻译文本。以下是需要翻译的内容：

有两个这样的单子实例，其中一个在“内部”是一个Mfunctor。

ms :: Monad m => m String
ms = undefined

tma :: (Monad m, MFunctor t) => t m a
tma = undefined

现在如果我尝试将ms与tma组合起来：

tmas = hoist (\ma -> comp ma ms) tma

我遇到了这个错误：

 Could not deduce (a ~ [Char])
    from the context (Monad m, MFunctor t)
      bound by the inferred type of
               comp :: (Monad m, MFunctor t) => t m b
      at Coroutine.hs:607:1-40
      `a' is a rigid type variable bound by
          a type expected by the context: m a -> m a at Coroutine.hs:607:8
    Expected type: m a
      Actual type: m String

这段文字的意思是：规定在Monad m中，ms :: Monad m => m a必须是任意类型的a。是否有一种方法可以将tma与特定参数的monad组合起来？

hoist的签名如下：

hoist :: (Monad m, MFunctor t) => (forall a. m a -> n a) -> t m b -> t n b

但是我无法想象 forall 如何影响我正在尝试做的事情，如果它有任何影响。

- xiaolingxiao

Answer 1

像这样将参数顺序切换为comp：

tmas = hoist (\ma -> comp ms ma) tma

-- or more simply:
tmas = hoist (comp ms) tma

原因是comp的类型是：

comp :: (Monad m) => m a -> m b -> m b

如果将第二个参数设置为ms，则b会被类型检查为String，您将得到以下结果：

(`comp` ms) :: (Monad m) => m a -> m String

...但是如果将ms设置为第一个参数，那么a将被类型检查为String，你将得到：

(ms `comp`) :: (Monad m) => m b -> m b

对于hoist，后一种类型是正确的，因为变量b是普遍量化的（即“forall”）。

关于正确性的问题，答案是普遍量化保证了传递给hoist的参数仅修改了单子层，而不是单子返回值。然而，如果您的意图也要修改返回值，则hoist并不是您想要的。

- Gabriella Gonzalez

Answer 2

hoistM :: MonadTrans t => (forall a. m a -> n a) -> t m b -> t n b

hoist函数的类型声明表明它期望一个函数 (forall a. m a -> n a)，即一个改变“容器”类型但保持类型参数不变的函数。这里的forall意味着您提供的函数不能针对任何特定的a进行专门化，而必须适用于任何类型参数。

您正在尝试使用的函数 (\ma -> comp ma ms) 的类型是 m a -> m String，因此它基本上与 hoist 期望的相反，因为它保持容器(m)不变，但改变了类型参数(从a到String)。

我认为在这种情况下，您实际上要寻找的不是hoist，而是将单子函数提升到在转换后的单子上工作的函数，因此您需要像下面这样的东西，而不是MFunctor：

hoistM :: MonadTrans t => (forall a. m a -> n a) -> t m b -> t n b

import Control.Monad.Trans.Class

tmas :: (Monad m, Monad (t m), MonadTrans t) => t m String
tmas = transLift (\ma -> comp ma ms) tma

transLift :: (Monad m, Monad (t m), MonadTrans t) => (m a -> m b) -> t m a -> t m b
transLift f tma = tma >>= lift . f . return

- shang

---

谢谢您的解释。forall 的存在是否能够保证某种程度的正确性呢？ - xiaolingxiao