Re: [Haskell-cafe] Re: Seeking advice about monadic traversal functions
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Seeking advice about monadic traversal functions
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Seeking advice about monadic traversal functions
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Seeking advice about monadic traversal functions
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
Re: [Haskell-cafe] Re: Seeking advice about monadic traversal functions
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Seeking advice about monadic traversal functions
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
Re: [Haskell-cafe] Re: Seeking advice about monadic traversal functions
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
