# 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. |