Hi Stephen, thanks for your reply: In the code above Tableau is the same type after rewriting. If that's
the case, maybe you don't need a state monad solution. However, if you are labelling something with /w/ which looks like an integer from your explanation, then first you want to make a variation of the Tableau datatype that holds the label, thus rewrite would be a type changing function:
rewrite :: Tableau -> Tableau'
I think the basic tableau data type would look like: data Tableau = Node (World, Expr) [Tableau] type World = Int and the rewrite function would need to track the current position of rewrite in the tableau and store a complete tableau (or some kind of record, possibly in a zipper) in order to move around, depending on the instruction it's given. So I would need something like: rewrite :: Tableau -> State (Record, Tableau) So that it could be passed an instruction such as: (Poss, [ex]) -> (a) inject ex into Tableau; (b) Store Tableau in Record; (c) move to correct spot in Record; (d) restart rewriting from position in Record. Even though Haskell's my first language, I still want a function that says: store current Tableau in *r, then get r* and restart.
If this is what you want to do, you should be able to thread "number supply" through the rewrite and rule functions fairly simply with a state monad.
rewrite :: Tableau -> State Int Tableau'
I think this means that when implementing the monad, I should define (>>=) as a general rule similar to the set of instructions above, e.g,. if f is a function that injects the list ex into a tree structure, and g is a rewrite function, then
= should have a structure abstracted from the following:
f >>= g = do f ~> State Record Tableau store Tableau in Record do g at Record make Record into current Tableau This seems similar to the "threading" method that, for instance, Wadler uses in the first sections of his paper on functional programming and monads, when building an evaluator that keeps track of division operations. Thanks or the response. If you see any glaring 'monadic errors,' I'd be happy to hear about them, but your advice was helpful :)