Backtrack over underlying monad in Monad Transformer

Question

As a side project I'm working on implementing my own Regex parser/compiler.

I figured that the actual matching portion would be a great time to learn how some backtracking monads work; like the list monad for example.

I ended up structuring my 'match' algorithm like so:

data Expr
  = Group Int Expr
  | Terms [Expr]
  | OneOf [Expr]
  | Repetition Expr Int (Maybe Int)
  | Empty
  | BackRef Int
  | Wildcard
  | Atom Char
  | Start
  | End
  deriving (Show)

data RState = RState
  { groups :: Groups
  , leftover :: String
  } deriving Show

match :: Expr -> ListT (State RState) String

where ListT is from Gabriel's List.Transformer lib

The State monad portion tracks the groups which have been captured (so that I can use them when I match on back-references) and the remaining string left to consume. The Expr is a data-structure representing the Regex as an AST of sorts.

Anyways; this works well; I recurse trying to make matches, if the match succeeds I return the matched portion as a result and alter the leftovers and groups in state accordingly, this ends up working in non-determinism because it will keep trying to continue using all possible previous matches when trying to process the next part of the regex. The problem is that it only backtracks on previous results, but NOT to the previous state! As a result my alternative match code for matching chains of optionals in the regex (e.g. a|b*|c; where each part is a 'term') looks like this:

match (OneOf terms) = do
  st <- get
  -- Backtrack the state and try again on each alternative
  let try t = put st >> match t
  asum (try <$> terms)

basically I try to match on each term, but even if the match fails it still alters state! So I need to manually rewind state in between failures. This is due to the ListT implementation of <|>:

ListT m <|> l = ListT (do
    s <- m
    case s of
        Nil       -> next l
        Cons x l' -> return (Cons x (l' <|> l)) )

Where we see it runs the underlying monad and continues in the same context.

I want something similar to this:

ListT m <|> l = ListT (do
    st <- get
    s <- m
    case s of
        Nil       -> put st >> next l
        Cons x l' -> return (Cons x (l' <|> l)) )

... But for all monad effects in general; I'm not even sure if this is possible.

I looked into the Logic Monad as a possible solution, but even after reading the paper I can't quite tell whether it can do what I want, maybe it's possible using ifte?

Is there a backtracking monad which not only backtracks the result of the monad, but also the monadic computations? I suppose this is impossible for things like IO, but should in theory be possible for pure monads? I guess that means it's not possible in general, but is there a type-class I could implement to gain this functionality for my case?

Thanks! I know I'm rambling out loud here, thanks for helping me think through this!

Answer 1

The solution is to invert the stack, as @danidiaz suggests.

I find it helpful to remember that outer monad transformers are at the mercy of inner ones. So SomeMonadT (State s) will be a "single-threaded" in its statefulness, no matter what SomeMonadT does.

An illuminating example is unrolling the StateT monad transformer over some other monad. Let's say we have:

foo :: StateT S M A
bar :: StateT S M B

do a <- foo
   b <- bar
   return (a,b)

This is just a fancy way of writing:

foo :: S -> M (A, S)
bar :: S -> M (B, S)

\s1 -> do 
    (a,s2) <- foo s1
    (b,s3) <- bar s2
    return ((a,b),s3)

Which is the familiar pattern motivating the State monad, except that the pattern takes place within another monadic context. That context is king, there is nothing the transformer can do about it.

That means ListT (State s) is a computation that tracks one state s, and then there is some "sugar" on top which is defined by ListT. You could think of it as an implementation of nondeterminism in a stateful machine (that only has the ability to track a single state).

Whereas StateT s [] is a computation that is essentially nondeterministic, and then there is some "sugar" which emulates a state. The underlying machine is a nondeterministic backtracking machine, and then the transformer uses a coding pattern to simulate state on that machine.

Here is a diagram by Dan Piponi that helps give some intuition:

This is a bit wishywashy and intuitive feeling territory, so I hope this was helpful.

Further reading: How to design a monadic stack?