haskell - 需要 MonadPlus (ST a) 实例

Question

我在看论文 Typed Logical Variables in Haskell ，但我无法理解最终实现的细节。特别是第 4 节中介绍的回溯状态转换器。出于某种原因，我不知道，GHC 认为我需要一个 MonadPlus (ST a) 的实例在函数中 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 ，或 mzero 上的一些变体, 是合适的函数。我只是不知道合适的功能是什么。我想知道的是我是否应该制作 MonadPlus (ST a)实例或者我没有使用正确的功能，并且误读了一些东西。

Answer 1

mzero是类型类 MonadPlus 的成员.特别是

mzero :: MonadPlus m => m a

用于您的函数的 monad unify是 LP ，实际上是 BackT用 ST 实例化.您还定义了一个 MonadPlus 的实例为 BackT ，这取决于底层 monad 的这样一个实例。自 ST没有这样的例子，GHC mock 你。

这是重要的部分:

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

简单的英语:这是 MonadPlus 的一个实例为 BackT m ，前提是 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

这个实例基本上连接了两个输出列表。我希望它适合您的需求。