Requires MonadPlus (ST a) Instance

Question

I'm reading the paper Typed Logical Variables in Haskell, but I'm failing to understand the details of the ultimate implementation. In particular, the backtracking state transformer introduced in section 4. For some reason, unknown to me, GHC believes I require a MonadPlus instance for (ST a) in the function unify, below:

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

I'm unsure what the problem is, and how to fix it. I was under the impression that I understood the preceding discussion and code until this point, but apparently I was mistaken. If someone could point out what's going awry - do I need a MonadPlus (ST a) instance or not? - it would be very helpful.

[EDIT: Clarification] I should have pointed out that the authors appear to claim that mzero, or some variation on mzero, is the appropriate function. I just don't know what the appropriate function is. What I'm wondering is whether I am supposed to make a MonadPlus (ST a) instance or I'm not using the correct function, and have misread something.

The return type of `unify` is `LP s ()`, or `BackT (ST a) ()`. So apparently the `BackT m` instance of `MonadPlus` requires `MonadPlus m`. Could you include that instance here? — Sjoerd Visscher, Oct 06 '11 at 23:06

fuz · Accepted Answer · 2011-10-06T23:24:19.507

4

mzero is a member of the typeclass MonadPlus. In particular

mzero :: MonadPlus m => m a

The monad that is used for your function unify is LP, which is actually BackT instantiated with ST. You furthermore define an instance of MonadPlus for BackT, that depends on such an instance for the underlying monad. Since ST has no such instance, GHC mocks you.

This is the important part:

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

In plain english: This is an instance of MonadPlus for BackT m, provided that m is also an instance of MonadPlus. Since m is instanciated with ST, you need that instance for ST. I wonder how you could define a sensible instance of MonadPlus without delegation. I have an idea:

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

This instance basically concatenates the two output lists. I hope it suits your needs.

edited Oct 06 '11 at 23:24

answered Oct 06 '11 at 23:08

fuz

88,405
25
200
352

You're correct; I've updated my post to include the definitions. It's possible I've misunderstood the monad and defined bind, return, mzero or plus incorrectly. – emi Oct 06 '11 at 23:11
This works perfectly. Thank you for explaining the problem and the solution. – emi Oct 06 '11 at 23:20
1

Be careful! This MonadPlus definition may not be what you expect. Intermediate writes to `STRef`s in a branch that eventually fails will *not* roll back. – luqui Oct 07 '11 at 01:22
@luqui is correct; if you try and use the regular `writeSTRef` in one branch, its effects will be seen in the other. To avoid this, use the `writeLPRef` definition in section 4.2. It wraps the `BackT` continuation in what's essentially a failure continuation in order to make `mplus` for `ST` seem commutative. This is just a matter of discipline, though, rather than `ST` really being a well-behaved `MonadPlus` instance. – acfoltzer Oct 09 '11 at 17:24

score 3 · Answer 2 · answered Oct 06 '11 at 23:19

3

The BackT MonadPlus instance probably should use the MonadPlus instance of [] instead of m, like this:

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

answered Oct 06 '11 at 23:19

Sjoerd Visscher

11,840
2
47
59

Requires MonadPlus (ST a) Instance

2 Answers2