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.