Problem with backtracking monad transformer

30 Jan 2003

      I'm trying to make a backtracking state monad using Ralf Hinze's
backtracking monad transformer.  My problem is that it won't backtrack
very far.

Suppose I try ( a >> b ) `mplus` c.

If b fails, it should try c, but it doesn't rewind past a.

My sample code is below.

GHCI> c [0,1] match_1            -- (1 or 0) then 1, OK
GHCI> c [1,0] match_2            -- (1 then 0) or (1,1), OK
GHCI> c [1,1] match_2            -- (1 then 0) or (1,1), fails

What have I misunderstood?

cheers,
Simon
(A disclaimer in an attachment?  - it wasn't my idea.)

-- backtracking state monad
-- requires -fglasgow-exts

import qualified Monad as M
import qualified Control.Monad.Trans as MT

-- turn tracing on and off by uncommenting just one of the following lines
import Debug.Trace( trace )
--trace s x = x

--
-- Ralf Hinze's efficient backtracking monad transformer
--

newtype BACKTR m a
  = BACKTR { mkBACKTR :: (forall b. (a -> m b -> m b) -> m b -> m b) }

instance (Monad m) => Monad (BACKTR m) where
  return a = BACKTR (\c -> c a)
  m >>= k  = BACKTR (\c -> mkBACKTR m (\a -> mkBACKTR (k a) c))

-- We don't use a Backtr class, but do it with the MonadPlus class,
-- mzero is false (fail),
-- mplus is ¦ (orelse)
instance (Monad m) => M.MonadPlus (BACKTR m) where
  mzero         = BACKTR (\c -> id)
  m1 `mplus` m2 = BACKTR (\c -> mkBACKTR m1 c . mkBACKTR m2 c)

-- standard MonadTrans class has lift for promote, and doesn't have observe
instance MT.MonadTrans BACKTR where
  lift m = BACKTR (\c f -> m >>= \a -> c a f)

observe :: (Monad m) => BACKTR m a -> m a
observe m = mkBACKTR m (\a f -> return a) (fail "false")

--
-- State Monad
--

data SM st a = SM (st -> (a,st)) -- The monadic type

instance Monad (SM st) where
   -- defines state propagation
   SM c1 >>= fc2 = SM (\s0 -> let (r,s1) = c1 s0
                                  SM c2 = fc2 r in
                                 c2 s1)
   return k = SM (\s -> (k,s))

-- extracts the state from the monad
readSM :: SM st st
readSM = SM (\s -> (s,s))

-- updates the state of the monad
updateSM :: (st -> st) -> SM st () -- alters the state
updateSM f = SM (\s -> ((), f s))

-- run a computation in the SM monad
runSM :: st -> SM st a -> (a,st)
runSM s0 (SM c) = c s0

-- backtracking state monad
--
type NDSM st a = BACKTR (SM st) a

readNDSM :: NDSM st st
readNDSM = MT.lift readSM

updateNDSM :: (st -> st) -> NDSM st ()
updateNDSM f = MT.lift (updateSM f)

--run a computation in the NDSM monad
runNDSM :: st -> NDSM st a -> (a,st)
runNDSM s0 m = runSM s0 (observe m)

--
-- the state
--
type Bit = Int

data CState = CState
             { ok                :: Bool,
               remaining_data    :: [Bit],
               history           :: [String] -- log, kept in reverse
             } deriving Show

initState xs = CState True xs []

-- prepend a message in the log
logit :: CState -> String -> CState
logit s logmsg = s { history = logmsg : (history s) }

--
-- matching action
--
match_bits :: [Bit] -> NDSM CState ()
match_bits xs = do
   s <- readNDSM
   let s' = logit s ("attempt match_bits " ++ show xs
                     ++ " remaining: " ++ show (remaining_data s))

       s'' = if xs == take (length xs) (remaining_data s')
             then
                s' { remaining_data = drop (length xs) (remaining_data s') }
             else
                s' { ok = False }
   if ok s''
      then updateNDSM (\s -> s'')
      else trace (unlines $ "MATCH FAILED":(reverse $ history s'')) M.mzero

--
-- test routines
--

-- just fine
match_1 =
   (match_bits [1] `M.mplus` match_bits [0])
...
...
match_bits [1]
-- this one only rewinds past the [0] attempt, not the [1] attempt
match_2 =
   (  (match_bits [1] >> match_bits [0]) 
      `M.mplus` match_bits [1, 1] )

c :: [Bit] -> NDSM CState () -> ([Bit], [String])
c h hspec = 
   let (v, s) = runNDSM (initState h) hspec in
   case (ok s) of True -> ([], "ok":(reverse $ history s))
                  _    -> ([(negate)1], ["fail"])

Problem with backtracking monad transformer

Guest, Simon