MonadPlus Instance Required (ST a)

Question

I am reading an article on typed booleans in Haskell , but I don’t understand the details of the final implementation. In particular, the reverse tracking state transformer presented in Section 4. For some reason unknown to me, the GHC believes that the function (ST a) in unify requires a <20> instance of unify below:

 newtype BackT ma = BT { run :: forall b . (a -> m [b]) -> m [b] } instance (Monad m) => Monad (BackT m) where return a = BT (\k -> ka) BT m >>= f = BT (\k -> m (\a -> run (fa) 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 sa = LR s (Maybe a) data Atom s = VarA (Var s (Atom s)) | Atom String class Unify ba | a -> b where var :: a -> Maybe (Var ba) 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 am not sure what the problem is and how to fix it. I had the impression that up to this point I understood the previous discussion and the code, but apparently I was wrong. If someone can indicate what is happening, do I need an instance of MonadPlus (ST a) or not? - It would be very helpful.

[EDIT: Clarification] I should have pointed out that the authors seem to argue that mzero or some variation on mzero is a suitable function. I just don’t know what this function is. I am wondering if I should make an instance of MonadPlus (ST a) , or if I am not using the correct function, and something is misunderstood.

Answer 1

mzero is a member of the MonadPlus class. In particular,

 mzero :: MonadPlus m => ma 

The monad that is used for your unify function is an LP , which is actually a BackT created using ST . In addition, you define a MonadPlus instance for BackT , which depends on that instance for the main monad. Since ST does not have such an instance, the GHC is mocking 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 also an instance of MonadPlus . Since m initialized by ST , you need this instance for ST . I wonder how you could define a reasonable 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 <- fa gs <- ga return $ fs ++ gs 

This instance basically combines the two output lists. Hope this fits your needs.

Answer 2

Perhaps the BackT MonadPlus should use the MonadPlus [] instance instead of m , for example:

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