Unifying Theories of Generic Programming

Generic programming (GP) is a technique that exploits the inherent structure that exists in data, to automatically produce efficient and flexible algorithms that can be adapted to suit different needs. GP ensures that the structure of the data itself plays a central role in maintaining the correctness of these algorithms. The last two decades have witnessed a number of approaches to GP, differing in convenience, expressiveness and efficiency. The work on theoretical approaches can be split into roughly two overlapping periods: the first was sparked by the Algebra of Programming, which concentrates on an algebraic approach to programming using concepts from category theory, and the second might be characterised by the use Generic Haskell where the simply-typed lambda calculus is used to represent Haskell’s rich types.

The aim of this project is to build upon previous work in this field and significantly advance the state of the art of generic programming and thus programming in general, with the following objectives: theory – generalising and unifying the two major approaches to GP; specification – exploring novel approaches for the specification of generic programs; reasoning – providing the infrastructure for reasoning about generic programs, concisely and precisely; application – demonstrating that GP has far-reaching and important applications. The vision is to develop a unifying theory of generic programming to inform the design of future programming languages, by bringing together the advantages of previous work into a coherent whole.