Generic and Indexed Programming

Generic programming is about making programs more widely applicable via exotic kinds of parametrization—not just along the dimensions of values or of types, but also of things such as the shape of data, algebraic structures, strategies, computational paradigms, and so on. Indexed programming is a lightweight form of dependently typed programming, constraining flexibility by allowing one to state and check relationships between parameters: that the shapes of two arguments agree, that an encoded value matches some type, that values transmitted along a channel conform to the stated protocol, and so on. The two forces of genericity and indexing balance each other nicely, simultaneously promoting and controlling generality. The Generic and Indexed Programming project at Oxford was funded by the UK Engineering and Physical Sciences Research Council over the period 2006–2010 to explore the interaction between these two forces. The closing activity of the project took the form of a Spring School on Generic and Indexed Programming, held at Wadham College, Oxford, during March 22–24, 2010; this volume collects the revised lecture notes from the school. The school was—and these lecture notes are—aimed at doctoral students, researchers, and practitioners in programming languages and related areas. A good grounding is assumed in typed functional programming, as in Haskell or OCaml. Six lecturers from the programming languages community, each an acknowledged expert in their specialism, covered various aspects of generic and indexed programming; each gave about four hours’ lectures, distributed throughout the week of the school. Lecture notes from five of those six sets of lectures are included here: Nate Foster on three approaches to bidirectional programming, for specifying consistent mappings to and from a data representation Ralf Hinze on using adjunctions to unify and generalize a number of familiar generic recursion schemes Oleg Kiselyov on the typed tagless interpreter approach for encoding a typed object language in a typed meta-language Jeremy Siek on the debates that took place over the attempt to incorporate concepts in the revised C++ standard Stephanie Weirich on datatype- and arity-generic programming within a dependently typed language The sixth lecturer, Simon Peyton Jones, spoke on type functions in Haskell, and their use in generic programming; his lecture notes are represented by his chapter “Fun with Type Functions” with Oleg Kiselyov and Chung-chieh Shan in the book Reflections on the Work of C. A. R. Hoare, edited by Cliff Jones, Bill Roscoe, and Ken Wood (Springer, 2010, ISBN 978-1-84882-911-4) in honour of Sir Tony Hoare’s 75th birthday. Slides for all six sets of lectures are available on the school’s website http://www.cs.ox.ac.uk/projects/gip/school.html. I would like to express my sincere thanks to the six lecturers at the school, for the considerable effort they devoted to making the event a success; to their co-authors, for helping to write up the lecture notes; to the staff of Wadham College, especially Jan Trinder, for their hospitality in the college’s 400th year; to EPSRC, for their financial support; and last but not least, to the 41 participants, for making it all worthwhile