Understanding Idiomatic Traversals Backwards and Forwards

The paper is available via the ACM DL Author-ize feature here.

Authors: R. Bird, J. Gibbons, S. Mehner, T. Schrijvers, and J. Voigtländer
Published: In Haskell Symposium 2013 (Haskell'13, acceptance rate 13/33), Boston, Massachusetts, Proceedings, pages 25-36, ACM, September 2013.
DOI: 10.1145/2503778.2503781
BibTeX: BGMSV13.bib
Abstract: We present new ways of reasoning about a particular class of effectful Haskell programs, namely those expressed as idiomatic traversals. Starting out with a specific problem about labelling and unlabelling binary trees, we extract a general inversion law, applicable to any monad, relating a traversal over the elements of an arbitrary traversable type to a traversal that goes in the opposite direction. This law can be invoked to show that, in a suitable sense, unlabelling is the inverse of labelling. The inversion law, as well as a number of other properties of idiomatic traversals, is a corollary of a more general theorem characterising traversable functors as finitary containers: an arbitrary traversable object can be decomposed uniquely into shape and contents, and traversal be understood in terms of those. Proof of the theorem involves the properties of traversal in a special idiom related to the free applicative functor.
Download: UnderstandingIdiomaticTraversalsBackwardsAndForwards.pdf
Rights: Copyright held by the authors. Exclusive publishing license granted to ACM. This (authors') version of the work is posted here for your personal use; not for redistribution. The definitive version was published as indicated (cf. also http://doi.acm.org/10.1145/2503778.2503781). It is available via the ACM DL Author-ize feature here.
Slides: I gave a talk on this paper at IFIP WG 2.1 meeting #70, slides are here.