Generic and Indexed Programming

Generic programming is about increasing the flexibility of programs without compromising on safety. This is typically achieved through introducing new kinds of parametrization. A parametrized program abstracts from a family of different but related programs, which can be retrieved by different instantiations of the parameter. A type system for the parameters allows the programmer to express constraints on parameters, and to statically check both the parametrized generic program and its specific instantiations. Examples of this notion include higher-order programming (parametrization by a function), parametric polymorphism (by a type, used uniformly), ad-hoc polymorphism (by a type, with some constraints), abstract datatypes (by an interface), datatype-genericity (by the shape of data), and so on. Our recent work has concentrated on one instance of this scheme, namely datatype-generic programming, in which programs are parametrized by type constructors, for which suitable instantiations are "lists of" and "trees of". We have investigated both programming techniques (including reasoning about generic programs, and using them to capture design patterns precisely), and language mechanisms (particularly lightweight approaches: patterns for simulating highly-expressive techniques in familiar but apparently less-expressive languages). Our recent experience has led us to a number of insights; this current proposal seeks support to exploit them. Firstly, these lightweight techniques, which we have to date been embedding in Haskell's still relatively expressive type system, are in fact applicable to even less expressive but more popular mainstream languages such as Java and C#. Secondly, the techniques have more applications than we first thought; in particular, they offer a solution to the so-called "expression problem", and other challenges involving extensibility: safe combination of independent extensions along multiple dimensions. Thirdly, new developments in languages, such as Haskell's generalized algebraic datatypes (GADTs), are leading us towards what we might call indexed programming: values are used to capture and statically verify properties of programs. As a simple example, a type of fixed-length vectors is indexed by the length; more elaborate examples involve a type of finite automata indexed by their states, and a type of type-safe interpreters indexed by the type of expression they interpret. Indexed programming is related to our previous work on generic programming in two ways: it directly supports a flavour of generic programming, indexing programs by a representation of types; and it is another lightweight approach, a kind of lightweight dependently-typed programming, providing many of the benefits with only a fraction of the costs - rather than having to resort to full-blown theorem proving and entangling notions of "compile-time" and "run-time", the indices can be reflected at the type level and checked using only mild extensions to existing type checking algorithms. We propose six packages of work implementing this vision: case studies on programming with indices; using McBride and Paterson's applicative functors to extend the "Scrap your Boilerplate" approach to generic programming to apply also to GADTs; applying GADTs to express safe extensible functions and datatypes, solving a generalization of Wadler's expression problem; translating these results to mainstream languages such as Java and C#, and using them to implement a library of reusable code capturing some of the Gang of Four design patterns; providing mechanisms for statically inferring witnesses to property propositions, saving the programmer from having to invent and manipulate them; investigating the use of indexed programming techniques for integrating the languages used in different tiers of enterprise architectures, aiming for type-safe database and XML access.