Understanding Idiomatic Traversals Backwards and Forwards
The paper is available via the ACM DL Author-ize feature:
| 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: | http://dl.acm.org/authorize?6842945 (free) |
| Slides: | I gave a talk on this paper at IFIP WG 2.1 meeting #70, slides are here. |