The development of the FISh2 programming language brings together two complementary strands of research within a single, concise formalism. The first is generic programming, whose goal is to develop more powerful techniques for re-using programs without compromising program correctness. The second is to exploit information about the shapes of data structures to speed up data access and improve memory management.
Examples of generic programs include those for mapping a function over an arbitrary data structure, or for pretty-printing an arbitrary expression. In FISh2 this is achieved by basing the type system on the theory of categorical functors. While functors have been added to languages before, FISh2 (and its predecessor, FML) is the first to make functors central to the type system, which is necessary to fully exploit their power.
One of the costs of polymorphic programming even in ML and especially in a generic programming environment is that the more general programs run slower. One important cause is that polymorphic programs do not have direct access to their arguments, but must use indirection. Shape analysis is used to determine the shapes of the data structures being used, so that programs can be specialised to access data directly.
In FISh2 this is realised by associating to each expression an expression for its shape. Indeed, the shapes of data structures can be defined by a generic function. The shapes are computed before computing the data to be stored within them, which results in significant efficiency gains.
A research program of this breadth requires input and feedback from a number of research communities, e.g. category theory, type theory, lambda-calculus, programming language design, that are all well-represented in Edinburgh. In particular, this visit enabled Jay to develop a cleaner mechanism for defining generic programs, that is able to support a new and powerful type inference mechanism.
The results developed in the fellowship have been incorporated into the prototype of FISh2 and will soon be reported in the literature.