Generic and Indexed Programming

Generic programming is about increasing the flexibility of programswithout compromising on safety. This is typically achieved throughintroducing new kinds of parametrization. A parametrized programabstracts from a family of different but related programs, which canbe retrieved by different instantiations of the parameter. A typesystem for the parameters allows the programmer to express constraintson parameters, and to statically check both the parametrized genericprogram and its specific instantiations. Examples of this notioninclude higher-order programming (parametrization by a function),parametric polymorphism (by a type, used uniformly), ad-hocpolymorphism (by a type, with some constraints), abstract datatypes(by an interface), datatype-genericity (by the shape of data), and soon.Our recent work has concentrated on one instance of this scheme,namely datatype-generic programming, in which programs areparametrized by type constructors, for which suitable instantiationsare lists of and trees of . We have investigated both programmingtechniques (including reasoning about generic programs, and using themto capture design patterns precisely), and language mechanisms(particularly lightweight approaches: patterns for simulatinghighly-expressive techniques in familiar but apparentlyless-expressive languages).Our recent experience has led us to a number of insights; this currentproposal seeks support to exploit them. Firstly, these lightweighttechniques, which we have to date been embedding in Haskell's stillrelatively expressive type system, are in fact applicable to even lessexpressive but more popular mainstream languages such as Java and C#.Secondly, the techniques have more applications than we firstthought; in particular, they offer a solution to the so-called expression problem , and other challenges involving extensibility:safe combination of independent extensions along multipledimensions.Thirdly, new developments in languages, such as Haskell'sgeneralized algebraic datatypes (GADTs), are leading us towards whatwe might call indexed programming: values are used to capture andstatically verify properties of programs. As a simple example, atype of fixed-length vectors is indexed by the length; moreelaborate examples involve a type of finite automata indexed bytheir states, and a type of type-safe interpreters indexed by thetype of expression they interpret. Indexed programming is related to our previous work on genericprogramming in two ways: it directly supports a flavour of genericprogramming, indexing programs by a representation of types; and it isanother lightweight approach, a kind of lightweight dependently-typedprogramming, providing many of the benefits with only a fraction ofthe costs - rather than having to resort to full-blown theorem provingand entangling notions of compile-time and run-time , the indicescan be reflected at the type level and checked using only mildextensions to existing type checking algorithms.We propose six packages of work implementing this vision: case studieson programming with indices; using McBride and Paterson's applicativefunctors to extend the Scrap your Boilerplate approach to genericprogramming to apply also to GADTs; applying GADTs to express safeextensible functions and datatypes, solving a generalization ofWadler's expression problem; translating these results to mainstreamlanguages such as Java and C#, and using them to implement a libraryof reusable code capturing some of the Gang of Four design patterns;providing mechanisms for statically inferring witnesses to propertypropositions, saving the programmer from having to invent andmanipulate them; investigating the use of indexed programmingtechniques for integrating the languages used in different tiers ofenterprise architectures, aiming for type-safe database and XMLaccess.