Be Kind‚ Rewind: A Modest Proposal about Traversal

A recent paper by Graham Hutton and Diana Fulger (\"Reasoning about Effects: Seeing the Wood through the Trees\", in the preproceedings of Trends in Functional Programming 2008) addresses the problem of reasoning about effectful functional programs, introducing a relabelling function on binary trees as a representative illustration. The example is a very fruitful one, but we argue that their approach is less effective than it might be, because they miss two opportunities for higher-level reasoning: abstraction from the particular kinds of effect (the choice of monad) and from the pattern of recursion (the flow of computation). We present an alternative approach using properties of idiomatic traversals, which cleanly separate the twin concerns of the kinds of effect and the pattern of recursion. In particular, we approach the problem by considering its inverse; and we argue that this is an important approach which has so far been missing from discussions of idiomatic traversal