Generic programming with fixed points for mutually recursive datatypes

Alexey Rodriguez, Stefan Holdermans, Andres Löh and Johan Jeuring

The 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009)
Edinburgh, Scotland, 31st August - 2nd September 2009

---

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.

---

START Conference Manager (V2.56.8 - Rev. 748M)