[Haskell-cafe] Seeking advice about monadic traversal functions

[Darryn Reid]

Hi, I hope that this is an appropriate place to post this question; I
initially posted to Haskell-beginners since that seemed appropriate to
my knowledge level. Brent Yorgey kindly suggested I should post here
instead.

Just for a little background: I'm an experienced computer scientist and
mathematician but am very new to Haskell (I love it, I might add, but
have much to learn).

I've coded a (fairly) general rewriting traversal - I suspect the
approach might be generalisable to all tree-like types, but this doesn't
concern me much right now. My purpose is for building theorem provers
for a number of logics, separating the overall control mechanism from
the specific rules for each logic.

The beauty of Haskell here is in being able to abstract the traversal
away from the specific reduction rules and languages of the different
logics. I have paired down the code here to numbers rather than modal
formulas for the sake of clarity and simplicity. My question is
two-fold:
1. Does my representation of the traversal seem good or would it be
better expressed differently? If so, I'd appreciate the thoughts of more
experienced Haskell users.
2. I cannot really see how to easily extend this to a queue-based
breadth-first traversal, which would give me fairness. I'm sure others
must have a good idea of how to do what I'm doing here except in
breadth-first order; I'd appreciate it very much if someone could show
me how to make a second breadth-first version.

Thanks in advance for any help!

Darryn.

start of code.
-------------------------------------------------------------------------
import Control.Monad
import Control.Monad.Identity

-- Tableau is a tree containing formulas of type a, in 
-- Fork (disjunctive) nodes and Single (conjunctive) nodes.
-- Paths from root to Nil each represent an interpretation.
data Tableau a =   Nil                           -- End of a path
                 | Single a (Tableau a)          -- Conjunction
                 | Fork (Tableau a) (Tableau a)  -- Disjunction
                 deriving (Eq, Show)

-- 'Cut' directs the traversal to move back up the tree rather than into
-- the current subtree, while 'Next' directs the traversal to proceed
-- into the subtree.
data Action = Cut | Next 
              deriving (Eq, Show)

-- The type of the rewrite function to perform at each node in
-- the traversal of the tree. The Rewriter returns the new
-- subtree to replace the existing subtree rooted at the
-- traversal node, and a direction controlling the traversal
-- to the next node.
type Rewriter m a = Tableau a -> m (Tableau a, Action)

-- The traversal function, depth-first order.
rewrite :: (Monad m) => Rewriter m a -> Tableau a -> m (Tableau a)
rewrite rf t = do (t', d) <- rf t
                  rewrite' rf d t'

-- Worker function for traversal, really its main body.
rewrite' :: (Monad m) => Rewriter m a -> Action -> Tableau a -> m
(Tableau a)
rewrite' rf Cut  t             = return t
rewrite' rf Next Nil           = return Nil
rewrite' rf Next (Single x t1) = do t1' <- rewrite rf t1
                                    return (Single x t1')
rewrite' rf Next (Fork t1 t2)  = do t1' <- rewrite rf t1
                                    t2' <- rewrite rf t2
                                    return (Fork t1' t2')

-- Some examples to test the code with:
-- ghci> let t0 = (Single 2 (Single 3 Nil))
-- ghci> let t1 = (Single 1 (Fork t0 (Fork (Single 4 Nil) (Single 5
Nil))))
-- ghci> let t2 = (Fork (Single 10 Nil) (Single 11 Nil))
-- ghci> let t3 = (Fork (Single 3 Nil) (Single 3 Nil))

-- Running "test4 t1 t2" produces the expected result; running 
-- "test4 t1 t3" does not terminate, because this endlessly 
-- generates new patterns that match the substitution condition:
test4 :: (Num t) => Tableau t -> Tableau t -> Tableau t
test4 tab tab' = runIdentity (rewrite rf tab)
            where rf (Single 3 Nil) = return (tab', Next)
                  rf t              = return (t, Next)

-- Running "test5 t1 t3", however, does terminate because the "Cut"
-- prevents the traversal from entering the newly spliced subtrees
-- that match the pattern.
test5 :: (Num t) => Tableau t -> Tableau t -> Tableau t
test5 tab tab' = runIdentity (rewrite rf tab)
            where rf (Single 3 Nil) = return (tab', Cut)
                  rf t              = return (t, Next)
-------------------------------------------------------------------------
end of code.