Generic programming with fixed points for mutually recursive datatypes

ABSTRACT

Many datatype-generic functions need access to the recursive positions in the structure of the datatype, and therefore adopt a fixed point view on datatypes. Examples include variants of fold that traverse the data following the recursive structure, or the Zipper data structure that enables navigation along the recursive positions. However, Hindley-Milner-inspired type systems with algebraic datatypes make it difficult to express fixed points for anything but regular datatypes. Many real-life examples such as abstract syntax trees are in fact systems of mutually recursive datatypes and therefore excluded. Using Haskell's GADTs and type families, we describe a technique that allows a fixed-point view for systems of mutually recursive datatypes. We demonstrate that our approach is widely applicable by giving several examples of generic functions for this view, most prominently the Zipper.

REFERENCES

• 1: T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In Generic Programming, pages 1--20. Kluwer, 2003.
• 2: A. Baars and D. Swierstra. Typing dynamic typing. In ICFP'02, pages 157--166, 2002.
• 3: M. Benke, P. Dybjer, and P. Jansson. Universes for generic programs and proofs in dependent type theory. Nordic J. of Comp., 10 (4): 265--289, 2003.
• 4: R. Bird and R. Paterson. Generalised folds for nested datatypes. Formal Aspects of Computing, 11: 11--2, 1999.
• 5: C. Böhm and A. Berarducci. Automatic synthesis of typed Λ-programs on term algebras. Theoretical Computer Science, 39: 135--154, 1985.
• 6: B. Bringert and A. Ranta. A pattern for almost compositional functions. In ICFP'06, pages 216--226, 2006.
• 7: J. Cheney and R. Hinze. A lightweight implementation of generics and dynamics. In ACM SIGPLAN Haskell Workshop, 2002.
• 8: J. Gibbons. Generic downwards accumulations. SCP, 37 (1--3): 37--65, 2000.
• 9: R. Hinze. A new approach to generic functional programming. In POPL'00, pages 119--132, 2000\natexlaba.
• 10: R. Hinze. Polytypic values possess polykinded types. In MPC'00, volume 1837 of LNCS, pages 2--27. Springer, 2000\natexlabb.
• 11: R. Hinze. Generics for the masses. In ICFP'04, pages 236--243, 2004.
• 12: R. Hinze, J. Jeuring, and A. Löh. Type-indexed data types. SCP, 51 (2): 117--151, 2004.
• 13: S. Holdermans, J. Jeuring, A. Löh, and A. Rodriguez. Generic views on data types. In MPC'06, volume 4014 of LNCS, pages 209--234. Springer, 2006.
• 14: G. Huet. The Zipper. JFP, 7 (5): 549--554, 1997.
• 15: P. Jansson and J. Jeuring. A framework for polytypic programming on terms, with an application to rewriting. In WGP'00, 2000.
• 16: P. Jansson and J. Jeuring. PolyP -- a polytypic programming language extension. In POPL'97, pages 470--482, 1997.
• 17: P. Jansson and J. Jeuring. Polytypic unification. JFP, 8 (5): 527--536, 1998.
• 18: J. Jeuring. Polytypic pattern matching. In FPCA'95, pages 238--248, 1995.
• 19: P. Johann and N. Ghani. Foundations for structured programming with GADTs. In POPL'08, pages 297--308, 2008.
• 20: P. Johann and N. Ghani. Initial algebra semantics is enough! In Proceedings, Typed Lambda Calculus and Applications, pages 207--222, 2007.
• 21: R. Lammel and S. Peyton Jones. Scrap your boilerplate: A practical design pattern for generic programming. pages 26--37. ACM Press, 2003.
• 22: R. Lammel, J. Visser, and J. Kort. Dealing with large bananas. In WGP'00, 2000.
• 23: A. Löh. Exploring Generic Haskell. PHD thesis, Utrecht University, 2004.
• 24: G. Malcolm. Data structures and program transformation. SCP, 14: 255--279, 1990.
• 25: C. McBride. Clowns to the left of me, jokers to the right (pearl): dissecting data structures. In POPL'08, pages 287--295, 2008.
• 26: C. McBride. The derivative of a regular type is its type of one-hole contexts. strictlypositive.org/diff.pdf, 2001.
• 27: E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes, and barbed wire. In FPCA'91, volume 523 of LNCS, pages 124--144. Springer, 1991.
• 28: N. Mitchell and C. Runciman. Uniform boilerplate and list processing. In ACM SIGPLAN Haskell Workshop, 2007.
• 29: P. Morris, T. Altenkirch, and C. McBride. Exploring the regular tree types. In Types for Proofs and Programs, LNCS. Springer, 2006.
• 30: T. Noortvan Noort, A. Rodriguez, S. Holdermans, J. Jeuring, and B. Heeren. A lightweight approach to datatype-generic rewriting. In WGP'08, 2008.
• 31: U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.
• 32: U. Norell and P. Jansson. Polytypic programming in Haskell. In IFL'03, volume 3145 of LNCS, pages 168--184. Springer, 2004.
• 33: B. C. d. S. Oliveira and J. Gibbons. Typecase: A design pattern for type-indexed functions. In ACM SIGPLAN Haskell Workshop, 2005.
• 34: B. C. d. S. Oliveira, R. Hinze, and A. Löh. Extensible and modular generics for the masses. In H. Nilsson, editor, TFP'06, pages 199--216, 2006.
• 35: S. Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge, 2003.
• 36: S. Peyton Jones, D. Vytiniotis, S. Weirich, and G. Washburn. Simple unification-based type inference for GADTs. In ICFP'06, pages 50--61, 2006.
• 37: A. Rodriguez. Towards Getting Generic Programming Ready for Prime Time. PhD thesis, Utrecht University, 2009.
• 38: T. Schrijvers, S. Peyton Jones, M. Chakravarty, and M. Sulzmann. Type checking with open type functions. In ICFP'08, pages 51--62, 2008.
• 39: T. Sheard and L. Fegaras. A fold for all seasons. In FPCA'93, pages 233--242, 1993.
• 40: T. Sheard and S. Peyton Jones. Template meta-programming in Haskell. In ACM SIGPLAN Haskell Workshop, 2002.
• 41: D. Swierstra, P. Azero, and J. Saraiva. Designing and implementing combinator languages. In AFP, volume 1608 of LNCS, pages 150--206. Springer, 1999.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.13 Reusable Software
            Subjects: Reusable libraries
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Design, Languages

Keywords:
datatype-generic programming, fixed points, haskell, mutually recursive datatypes