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.
mzero
is a member of the typeclassMonadPlus
. In particularThe monad that is used for your function
unify
isLP
, which is actuallyBackT
instantiated withST
. You furthermore define an instance ofMonadPlus
forBackT
, that depends on such an instance for the underlying monad. SinceST
has no such instance, GHC mocks you.This is the important part:
In plain english: This is an instance of
MonadPlus
forBackT m
, provided thatm
is also an instance ofMonadPlus
. Sincem
is instanciated withST
, you need that instance forST
. I wonder how you could define a sensible instance ofMonadPlus
without delegation. I have an idea:This instance basically concatenates the two output lists. I hope it suits your needs.