Seeking advice about monadic traversal functions
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.
Darryn Reid wrote:
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.
Looks fine to me, though I have no experience with tree rewriting. :) I'd probably write it like this:
data Tableau a = Nil -- End of a path | Single a (Tableau a) -- Conjunction | Fork (Tableau a) (Tableau a) -- Disjunction deriving (Eq, Show) data Action = Cut | Next type Rewriter m a = Tableau a -> m (Tableau a, Action)
rewrite :: (Monad m) => Rewriter m a -> Tableau a -> m (Tableau a) rewrite f t = f t >>= (uncurry . flip) go where go Cut t = return t go Next Nil = return Nil go Next (Single x t1) = liftM (Single x) (rewrite f t1) go Next (Fork t1 t2 ) = liftM2 Fork (rewrite f t1) (rewrite f t2) In particular, liftM and liftM2 make it apparent that we're just wrapping the result in a constructor. In case you want more flexibility in moving from children to parents, you may want to have a look at zippers http://en.wikibooks.org/wiki/Haskell/Zippers
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.
This is more tricky than I thought! Just listing the nodes in breadth-first order is straightforward, but the problem is that you also want to build the result tree. Depth-first search follows the tree structure more closely, so building the result was no problem. The solution is to solve the easy problem of listing all nodes in breadth-first order first, because it turns out that it's possible to reconstruct the result tree from such a list! In other words, it's possible to run breadth-first search in reverse, building the tree from a list of nodes. How exactly does this work? If you think about it, the analogous problem for depth-first search is not too difficult, you just walk through the list of nodes and build a stack; pushing Nil nodes and combining the top two items when encountering Fork nodes. So, for solving the breadth-first version, the idea is to build a queue instead of a stack. The details of that are a bit tricky of course, you have to be careful when to push what on the queue. But why bother being careful if we have Haskell? I thus present the haphazardly named: Lambda Fu, form 132 - linear serpent inverse The idea is to formulate breadth-first search in a way that is *trivial* to invert, and the key ingredient to that is a *linear* function, i.e. one that never discards or duplicates data, but only shuffles it around. Here is what I have in mind: {-# LANGUAGE ViewPatterns #-} import Data.Sequence as Seq -- this will be our queue type import Data.List as List type Node a = Tableau a -- just a node without children (ugly type) type State a = ([Action],[(Action,Node a)], Seq (Tableau a)) queue (_,_,q) = q nodes (_,l,_) = l analyze :: State a -> State a analyze (Cut :xs, ts, viewl -> t :< q) = (xs, (Cut , t ) : ts, q ) analyze (Next:xs, ts, viewl -> Nil :< q) = (xs, (Next, Nil ) : ts, q ) analyze (Next:xs, ts, viewl -> Single x t1 :< q) = (xs, (Next, Single x u) : ts, q |> t1 ) analyze (Next:xs, ts, viewl -> Fork t1 t2 :< q) = (xs, (Next, Fork u u ) : ts, (q |> t1) |> t2 ) u = Nil -- or undefined bfs xs t = nodes $ until (Seq.null . queue) analyze (xs,[],singleton t) So, bfs just applies analyze repeatedly on a suitable state which includes the queue, the list of nodes in breadth-first order and a stream of actions. (This is a simplified example, you will calculate the actions on the fly of course.) To be able to pattern match on the queue, I have used GHC's ViewPattern extension. It should be clear that analyze performs exactly one step of a breadth-first traversal. Now, the key point is that analyze is *linear*, it never discards or duplicates any of the input variables, it just shuffles them around, like moving a constructor from the tree to the node list or from one list to the other. This makes it straightforward to implement an inverse function synthesize which fulfills synthesize . analyze = id After all, we only have to write the definition of analyze from right to left! synthesize :: State a -> State a synthesize (xs, (Cut , t ) : ts, q) = (Cut:xs , ts, t <| q) synthesize (xs, (Next, Nil ) : ts, q) = (Next:xs, ts, Nil <| q) synthesize (xs, (Next, Single x _) : ts, viewr -> q :> t1) = (Next:xs, ts, Single x t1 <| q) synthesize (xs, (Next, Fork _ _ ) : ts, viewr -> (viewr -> q :> t1) :> t2) = (Next:xs, ts, Fork t1 t2 <| q) Looks a bit noisy, but I have simply copy & pasted the four equations for analyze and interchanged the left-hand and the right-hand sides, adjusting the view patterns. Thus, we can invert bfs by repeatedly applying synthesize to the final state of bfs : unBfs ts = (`index` 0) . queue $ until (List.null . nodes) synthesize ([],ts,empty) By construction, we have obtained the desired unBfs . bfs xs = id Regards, Heinrich Apfelmus PS: * I have used a double-ended queue, but we're never really using both ends at once. An ordinary FIFO queue will suffice if we interpret it to "change direction" between bfs and unBfs . * Exchanging the queue for a stack will give depth-first search and its inverse. -- http://apfelmus.nfshost.com
Heinrich, Thanks for your excellent response! Indeed, it was the rebuilding of the tree that had me stumped. I also see the benefits of using the lift functions, thanks again for this insight. Darryn. On Wed, 2010-03-31 at 12:44 +0200, Heinrich Apfelmus wrote:
Darryn Reid wrote:
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.
Looks fine to me, though I have no experience with tree rewriting. :) I'd probably write it like this:
data Tableau a = Nil -- End of a path | Single a (Tableau a) -- Conjunction | Fork (Tableau a) (Tableau a) -- Disjunction deriving (Eq, Show) data Action = Cut | Next type Rewriter m a = Tableau a -> m (Tableau a, Action)
rewrite :: (Monad m) => Rewriter m a -> Tableau a -> m (Tableau a) rewrite f t = f t >>= (uncurry . flip) go where go Cut t = return t go Next Nil = return Nil go Next (Single x t1) = liftM (Single x) (rewrite f t1) go Next (Fork t1 t2 ) = liftM2 Fork (rewrite f t1) (rewrite f t2)
In particular, liftM and liftM2 make it apparent that we're just wrapping the result in a constructor.
In case you want more flexibility in moving from children to parents, you may want to have a look at zippers
http://en.wikibooks.org/wiki/Haskell/Zippers
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.
This is more tricky than I thought! Just listing the nodes in breadth-first order is straightforward, but the problem is that you also want to build the result tree. Depth-first search follows the tree structure more closely, so building the result was no problem.
The solution is to solve the easy problem of listing all nodes in breadth-first order first, because it turns out that it's possible to reconstruct the result tree from such a list! In other words, it's possible to run breadth-first search in reverse, building the tree from a list of nodes.
How exactly does this work? If you think about it, the analogous problem for depth-first search is not too difficult, you just walk through the list of nodes and build a stack; pushing Nil nodes and combining the top two items when encountering Fork nodes. So, for solving the breadth-first version, the idea is to build a queue instead of a stack.
The details of that are a bit tricky of course, you have to be careful when to push what on the queue. But why bother being careful if we have Haskell? I thus present the haphazardly named:
Lambda Fu, form 132 - linear serpent inverse
The idea is to formulate breadth-first search in a way that is *trivial* to invert, and the key ingredient to that is a *linear* function, i.e. one that never discards or duplicates data, but only shuffles it around. Here is what I have in mind:
{-# LANGUAGE ViewPatterns #-} import Data.Sequence as Seq -- this will be our queue type import Data.List as List
type Node a = Tableau a -- just a node without children (ugly type) type State a = ([Action],[(Action,Node a)], Seq (Tableau a)) queue (_,_,q) = q nodes (_,l,_) = l
analyze :: State a -> State a analyze (Cut :xs, ts, viewl -> t :< q) = (xs, (Cut , t ) : ts, q ) analyze (Next:xs, ts, viewl -> Nil :< q) = (xs, (Next, Nil ) : ts, q ) analyze (Next:xs, ts, viewl -> Single x t1 :< q) = (xs, (Next, Single x u) : ts, q |> t1 ) analyze (Next:xs, ts, viewl -> Fork t1 t2 :< q) = (xs, (Next, Fork u u ) : ts, (q |> t1) |> t2 ) u = Nil -- or undefined
bfs xs t = nodes $ until (Seq.null . queue) analyze (xs,[],singleton t)
So, bfs just applies analyze repeatedly on a suitable state which includes the queue, the list of nodes in breadth-first order and a stream of actions. (This is a simplified example, you will calculate the actions on the fly of course.) To be able to pattern match on the queue, I have used GHC's ViewPattern extension.
It should be clear that analyze performs exactly one step of a breadth-first traversal.
Now, the key point is that analyze is *linear*, it never discards or duplicates any of the input variables, it just shuffles them around, like moving a constructor from the tree to the node list or from one list to the other. This makes it straightforward to implement an inverse function synthesize which fulfills
synthesize . analyze = id
After all, we only have to write the definition of analyze from right to left!
synthesize :: State a -> State a synthesize (xs, (Cut , t ) : ts, q) = (Cut:xs , ts, t <| q) synthesize (xs, (Next, Nil ) : ts, q) = (Next:xs, ts, Nil <| q) synthesize (xs, (Next, Single x _) : ts, viewr -> q :> t1) = (Next:xs, ts, Single x t1 <| q) synthesize (xs, (Next, Fork _ _ ) : ts, viewr -> (viewr -> q :> t1) :> t2) = (Next:xs, ts, Fork t1 t2 <| q)
Looks a bit noisy, but I have simply copy & pasted the four equations for analyze and interchanged the left-hand and the right-hand sides, adjusting the view patterns.
Thus, we can invert bfs by repeatedly applying synthesize to the final state of bfs :
unBfs ts = (`index` 0) . queue $ until (List.null . nodes) synthesize ([],ts,empty)
By construction, we have obtained the desired
unBfs . bfs xs = id
Regards, Heinrich Apfelmus
PS: * I have used a double-ended queue, but we're never really using both ends at once. An ordinary FIFO queue will suffice if we interpret it to "change direction" between bfs and unBfs . * Exchanging the queue for a stack will give depth-first search and its inverse.
-- http://apfelmus.nfshost.com
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Darryn Reid wrote:
Heinrich,
Thanks for your excellent response! Indeed, it was the rebuilding of the tree that had me stumped. I also see the benefits of using the lift functions, thanks again for this insight.
My pleasure. :) By the way, there's also another, very flexible way to rebuild the tree: give each node a unique identifier. The traversal returns a list of labeled nodes with their children replaced by labels, like this: [(1,Nil),(2,Single 'a' 3),(3,Nil),(4,Fork 1 2),...] To rebuild the tree, simply put the list into a finite map and replace identifiers by proper trees again. However, this solution is essentially the same as using a mutable tree, the unique identifiers represent memory addresses. That's why I sought to reconstruct the tree from the structure of the traversal (using the same intermediate queue data structure, etc.). Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com
On 3/31/10 12:44, Heinrich Apfelmus wrote:
go Next (Single x t1) = liftM (Single x) (rewrite f t1) go Next (Fork t1 t2 ) = liftM2 Fork (rewrite f t1) (rewrite f t2)
In particular, liftM and liftM2 make it apparent that we're just wrapping the result in a constructor.
A small remark: I prefer using applicative notation for this:
go Next (Single x t1) = Single x <$> rewrite f t1 go Next (Fork t1 t2 ) = Fork <$> rewrite f t1 <*> rewrite f t2
Martijn.
Martijn, Thanks for your comment and advice. Could you explain a little further your thinking? Specifically, what advantage do you find in the applicative notation, and when would you advise using it and when would you advise not using it? Thanks again, I appreciate your help. Darryn. On Fri, 2010-04-02 at 20:26 +0200, Martijn van Steenbergen wrote:
On 3/31/10 12:44, Heinrich Apfelmus wrote:
go Next (Single x t1) = liftM (Single x) (rewrite f t1) go Next (Fork t1 t2 ) = liftM2 Fork (rewrite f t1) (rewrite f t2)
In particular, liftM and liftM2 make it apparent that we're just wrapping the result in a constructor.
A small remark: I prefer using applicative notation for this:
go Next (Single x t1) = Single x <$> rewrite f t1 go Next (Fork t1 t2 ) = Fork <$> rewrite f t1 <*> rewrite f t2
Martijn. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Darryn Reid wrote:
Martijn van Steenbergen wrote:
A small remark: I prefer using applicative notation for this:
go Next (Single x t1) = Single x <$> rewrite f t1 go Next (Fork t1 t2 ) = Fork <$> rewrite f t1 <*> rewrite f t2
Thanks for your comment and advice. Could you explain a little further your thinking? Specifically, what advantage do you find in the applicative notation, and when would you advise using it and when would you advise not using it?
The applicative notation is more general since it also applies to applicative functors http://www.cs.nott.ac.uk/~ctm/IdiomLite.pdf It's main advantage over the liftM family is that it can be used with any number of arguments liftM f m = f <$> m liftM2 f m n = f <$> m <*> n liftM3 f m n o = f <$> m <*> n <*> o etc. and that's why I prefer it as well. It's very similar to function application, too, just think of <*> as a replacement for the empty space that separates function arguments. The only drawback is probably that you have to import Control.Applicative In fact, it doesn't actually work for monads, I think you have to wrap it in a newtype. :D The same effect can be achieved with `ap` , though: liftM3 f m n p = return f `ap` m `ap` n `ap` o Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com
On 4/6/10 15:31, Heinrich Apfelmus wrote:
In fact, it doesn't actually work for monads, I think you have to wrap it in a newtype. :D The same effect can be achieved with `ap` , though:
Fortunately, by now most (standard) monads are also applicatives. :-) Besides generalizing to an arbitrary number of arguments, it uses infix operators which saves you some parentheses. Groetjes, Martijn.
participants (3)
-
Darryn Reid -
Heinrich Apfelmus -
Martijn van Steenbergen