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.
- R. Bird and L. Meertens. Nested datatypes. In Mathematics of Program Construction, volume 1422 of Lecture Notes in Computer Science, pages 52--67. Springer, 1998. 10.1007/BFb0054285. Google ScholarDigital Library
- P. Capriotti and A. Kaposi. Free applicative functors. University of Nottingham. http://paolocapriotti.com/blog/2013/04/03/free-applicative-functors/, Apr. 2013.Google Scholar
- N. Gambino and M. Hyland. Wellfounded trees and dependent polynomial functors. In Types for Proofs and Programs, volume 3085 of Lecture Notes in Computer Science, pages 210--225. Springer, 2004. 10.1007/978-3-540-24849-1_14.Google Scholar
- J. Gibbons and B. C. d. S. Oliveira. The essence of the Iterator pattern. Journal of Functional Programming, 19 (3,4): 377--402, 2009. 10.1017/S0956796809007291. Google ScholarDigital Library
- J.-Y. Girard. Normal functors, power series and ł-calculus. Annals of Pure and Applied Logic, 37 (2): 129--177, 1988. 10.1016/0168-0072(88)90025--5.Google ScholarCross Ref
- G. Hutton and D. Fulger. Reasoning About Effects: Seeing the Wood Through the Trees. In Trends in Functional Programming, pre-proceedings, Nijmegen, The Netherlands, 2008.Google Scholar
- M. Jaskelioff and O. Rypácek. An investigation of the laws of traversals. In Mathematically Structured Functional Programming, volume 76 of Electronic Proceedings in Theoretical Computer Science, pages 40--49, 2012. 10.4204/EPTCS.76.5.Google Scholar
- C. McBride and R. Paterson. Applicative programming with effects. Journal of Functional Programming, 18 (1): 1--13, 2008. 10.1017/S0956796807006326. Google ScholarDigital Library
- E. Moggi, G. Bellè, and B. Jay. Monads, shapely functors, and traversals. Electronic Notes in Theoretical Computer Science, 29: 187--208, 1999. 10.1016/S1571-0661(05)80316-0. Proceedings of Category Theory and Computer Science.Google ScholarCross Ref
- R. O'Connor and M. Jaskelioff. On the static nature of traversals. http://r6.ca/blog/20121209T182914Z.html, Dec. 2012.Google Scholar
- O. Rypácek. Labelling polynomial functors: A coherent approach. Manuscript, Mar. 2010.Google Scholar
- J. Voigtländer. Free theorems involving type constructor classes. In International Conference on Functional Programming, pages 173--184. ACM, 2009. 10.1145/1596550.1596577. Google ScholarDigital Library
- P. Wadler. Theorems for free! In Functional Programming Languages and Computer Architecture, pages 347--359. ACM, 1989. 10.1145/99370.99404. Google ScholarDigital Library
Index Terms
- Understanding idiomatic traversals backwards and forwards
Recommendations
Understanding idiomatic traversals backwards and forwards
Haskell '13We 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 ...
Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous
We revisit the connection between three notions of computation: Moggi s monads, Hughes s arrows and McBride and Paterson s idioms (also called applicative functors). We show that idioms are equivalent to arrows that satisfy the type isomorphism A B 1 (A ...
Algebraic effects and effect handlers for idioms and arrows
WGP '14: Proceedings of the 10th ACM SIGPLAN workshop on Generic programmingPlotkin and Power's algebraic effects combined with Plotkin and Pretnar's effect handlers provide a foundation for modular programming with effects. We present a generalisation of algebraic effects and effect handlers to support other kinds of effectful ...
Comments