Clowns to the left of me, jokers to the right (pearl): dissecting data structures

ABSTRACT

This paper introduces a small but useful generalisation to the 'derivative' operation on datatypes underlying Huet's notion of 'zipper', giving a concrete representation to one-hole contexts in data which is undergoing transformation. This operator, 'dissection', turns a container-like functor into a bifunctor representing a one-hole context in which elements to the left of the hole are distinguished in type from elements to its right.

I present dissection here as a generic program, albeit for polynomial functors only. The notion is certainly applicable more widely, but here I prefer to concentrate on its diverse applications. For a start, map-like operations over the functor and fold-like operations over the recursive data structure it induces can be expressed by tail recursion alone. Further, the derivative is readily recovered from the dissection. Indeed, it is the dissection structure which delivers Huet's operations for navigating zippers.

The original motivation for dissection was to define 'division', capturing the notion of leftmost hole, canonically distinguishing values with no elements from those with at least one. Division gives rise to an isomorphism corresponding to the remainder theorem in algebra. By way of a larger example, division and dissection are exploited to give a relatively efficient generic algorithm for abstracting all occurrences of one term from another in a first-order syntax. The source code for the paper is available online and compiles with recent extensions to the Glasgow Haskell Compiler.

REFERENCES

• 1: Michael Abbott , Thorsten Altenkirch , Neil Ghani, Containers: constructing strictly positive types, Theoretical Computer Science, v.342 n.1, p.3-27, 6 September 2005 [doi>10.1016/j.tcs.2005.06.002]
• 2: Michael Abbott , Thorsten Altenkirch , Conor McBride , Neil Ghani, ∂ for Data: Differentiating Data Structures, Fundamenta Informaticae, v.65 n.1-2, p.1-28, January 2005
• 3: Mads Sig Ager , Dariusz Biernacki , Olivier Danvy , Jan Midtgaard, A functional correspondence between evaluators and abstract machines, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.8-19, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888254]
• 4: William Aitken and John Reppy. Abstract value constructors. Technical Report TR 92-1290, Cornell University, 1992.
• 5: Michael Barr and Charles Wells. Toposes, Triples and Theories, chapter 9. Number 278 in Grundlehren der Mathematischen Wissenschaften. Springer, New York, 1984.
• 6: Richard Bird , Oege de Moor, Algebra of programming, Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 7: Richard S. Bird , Ross Paterson, de Bruijn notation as a nested datatype, Journal of Functional Programming, v.9 n.1, p.77-91, January 1999 [doi>10.1017/S0956796899003366]
• 8: Janusz A. Brzozowski, Derivatives of Regular Expressions, Journal of the ACM (JACM), v.11 n.4, p.481-494, Oct. 1964 [doi>10.1145/321239.321249]
• 9: Jean-Christophe Filliatre. Backtracking iterators. Technical Report 1428, CNRS-LRI, January 2006.
• 10: Jeremy Gibbons. Datatype-generic programming. In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, Spring School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science. Springer-Verlag, 2007. To appear.
• 11: Thomas Hallgren. Fun with functional dependencies. In Joint Winter Meeting of the Departments of Science and Computer Engineering, Chalmers University of Technology and Goteborg University, Varberg, Sweden., January 2001.
• 12: Ralf Hinze , Johan Jeuring , Andres Löh, Type-indexed data types, Science of Computer Programming, v.51 n.1-2, p.117-151, May 2004 [doi>10.1016/j.scico.2003.07.001]
• 13: Martin Hofmann , Steffen Jost, Static prediction of heap space usage for first-order functional programs, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.185-197, January 15-17, 2003, New Orleans, Louisiana, USA
• 14: Gérard Huet, The Zipper, Journal of Functional Programming, v.7 n.5, p.549-554, September 1997 [doi>10.1017/S0956796897002864]
• 15: Patrik Jansson , Johan Jeuring, PolyP—a polytypic programming language extension, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.470-482, January 15-17, 1997, Paris, France [doi>10.1145/263699.263763]
• 16: Andre Joyal. Foncteurs analytiques et especes de structures. In Combinatoire enumerative, number 1234 in LNM, pages 126--159. 1986.
• 17: Conor McBride. The Derivative of a Regular Type is its Type of One-Hole Contexts. Available at http://www.cs.nott.ac.uk/~ctm/diff.pdf, 2001.
• 18: Conor McBride, Faking it Simulating dependent types in Haskell, Journal of Functional Programming, v.12 n.5, p.375-392, July 2002 [doi>10.1017/S0956796802004355]
• 19: Matthias Neubauer, Peter Thiemann, Martin Gasbichler, and Michael Sperber. A Functional Notation for Functional Dependencies. In The 2001 ACM SIGPLAN Haskell Workshop, Firenze, Italy, September 2001.
• 20: Simon Peyton Jones, Mark Jones, and Erik Meijer. Type classes: an exploration of the design space. In Proceedings of the Haskell Workshop, Amsterdam, The Netherlands, June 1997.
• 21: P. Wadler , S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-76, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75283]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation

General Terms:
Algorithms, Design, Languages, Theory

Keywords:
datatype, differentiation, dissection, division, generic programming, iteration, polynomial, stack, tail recursion, traversal, zipper