需要 MonadPlus (ST a) 实例

Question

我正在阅读这篇论文在Haskell中使用类型化逻辑变量，但是我无法理解最终实现的细节。特别是第4节中介绍的回溯状态转换器。由于某种我不知道的原因，GHC认为我需要(ST a)的MonadPlus实例，在下面的unify函数中：

newtype BackT m a = BT { run :: forall b . (a -> m [b]) -> m [b] }

instance (Monad m) => Monad (BackT m) where
 return a   = BT (\k -> k a)
 BT m >>= f = BT (\k -> m (\a -> run (f a) k))

instance (MonadPlus m) => MonadPlus (BackT m) where 
 mzero             = BT (\s -> mzero)
 f `mplus` g = BT (\s -> (run f) s `mplus` (run g) s)

type LP a = BackT (ST a)
type LR   = STRef

type Var s a = LR s (Maybe a)   
data Atom s = VarA (Var s (Atom s)) | Atom String

class Unify b a | a -> b where
 var   :: a -> Maybe (Var b a)
 unify :: a -> a -> LP s ()

instance Unify s (Atom s) where
 var (VarA a) = Just a
 var _        = Nothing

 unify (Atom a) (Atom b) | a == b = return () -- type checks
 unify _        _                 = mzero     -- requires MonadPlus (ST a) instance

我不确定问题出在哪里，也不知道如何解决。在这之前的讨论和代码中，我以为自己已经理解了，但显然我错了。如果有人能指出问题所在——我是否需要一个 MonadPlus (ST a) 实例？——那将非常有帮助。 [编辑：澄清] 我应该指出，作者似乎声称，mzero或某种变体是适当的函数。我只是不知道适当的函数是什么。我想知道的是，我是否应该创建一个 MonadPlus (ST a) 实例，还是我没有使用正确的函数，误读了什么。

- emi

---

unify 的返回类型是 LP s () 或 BackT (ST a) ()。因此，显然 MonadPlus 的 BackT m 实例需要 MonadPlus m。你能在这里包含该实例吗？ - Sjoerd Visscher

Answer 1

mzero是MonadPlus类型类的成员。特别地，

mzero :: MonadPlus m => m a

你的函数 unify 使用的单子是 LP，实际上是使用了 ST 实例化的 BackT。你还为 BackT 定义了一个 MonadPlus 的实例，该实例依赖于底层单子的实例。由于 ST 没有这样的实例，GHC 会出现错误。

这是重要的部分：

instance (MonadPlus m) => MonadPlus (BackT m) where 
  mzero             = BT (\s -> mzero)
  f `mplus` g = BT (\s -> (run f) s `mplus` (run g) s)

简单地说，这是BackT m的一个MonadPlus实例，前提是m也是MonadPlus实例。由于m是用ST实现的，您需要ST实例。我想知道如何在没有委派的情况下定义一个合理的MonadPlus实例，我有一个想法：

instance MonadPlus (BackT m) where
  mzero = BT (const $ return [])
  mplus (BT f) (BT g) = BT $ \a -> do
    fs <- f a
    gs <- g a
    return $ fs ++ gs

这个实例基本上是将两个输出列表连接起来。希望它能满足您的需求。

- fuz

---

你是正确的；我已更新我的文章，包括这些定义。可能我误解了单子并且错误地定义了 bind、return、mzero 或 plus。 - emi

这个工作完美。感谢您解释问题和解决方案。 - emi

注意！ 这个MonadPlus定义可能不是您所期望的。在最终失败的分支中对STRef进行中间写入将不会回滚。 - luqui

@luqui是正确的；如果你尝试在一个分支中使用常规的writeSTRef，它的效果将会在另一个分支中被看到。为了避免这种情况，请在第4.2节中使用writeLPRef定义。它将BackT continuation包装在本质上是失败 continuation的东西中，以使得ST的mplus看起来是可交换的。然而，这只是一种纪律问题，而不是ST真正成为良好行为的MonadPlus实例。 - acfoltzer

Answer 2

BackT的MonadPlus实例可能应该使用[]的MonadPlus实例而不是m，如下所示：

instance (Monad m) => MonadPlus (BackT m) where 
  mzero       = BT (\_ -> return mzero)
  f `mplus` g = BT (\s -> liftM2 mplus (run f s) (run g s))

- Sjoerd Visscher