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 Mona开发者_如何学编程dPlus (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.
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.
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))
精彩评论