Categorical Foundations for Indexed Programming

Type systems have become an integral part of programming language design and implementation, leading to fundamental contributions in such areas as security, databases, and concurrent and distributed programming. Type systems provide information that can be used for such tasks as error detection, program optimisation, and memory management. A type system governs a programming language's classification of values and expressions into data types, which determines how data of those types can be manipulated and how those data can interact. Originally, type systems contained only simple data types like Int and Char for classifying basic data such as integers and characters. However, advanced type systems support sophisticated types that can guarantee not only that well-typed programs are free of simple errors, such as trying to add non-numeric expressions, but also that they preserve invariants, do not violate space or other constraints, can be optimised in principled ways, or satisfy other sophisticated correctness properties. Much of the effort in type systems research is aimed at closing the semantic gap between what programmers know about computational entities and what types can express about them.One of the most promising approaches to increasing the expressiveness and reasoning power of type systems is to allow types to be indexed by other information. For example, rather than simply having a type List denoting the list data type, list types can be indexed by additional information that can be used to detect more errors, perform more optimisations, and provide greater guarantees of correctness than would otherwise be possible. The extra information in the indices thus helps close the aforementioned semantic gap.Indexed programming is the practice of programming with indexed types. Perhaps the most common form of indexing is indexing types by other types. To model lists of integers or lists of booleans or lists of lists of data of type t, for example, type-indexed types such as List Int or List Bool or List (List t) can be used. More recently, programming languages have been developed which allow types to be indexed not just by other types, but also by terms. For example, to model lists of length 3 or lists that a particular proof p proves are sorted, term-indexed types such as List 3 or List p can be used. The practice of indexed programming has now advanced to the stage where principled foundations are required to take the subject further. The aim of the proposed research is to develop a categorical foundation of indexed programming. That is, it aims to improve the understanding of, and the ability to solve specific problems involving traditional term-indexed and type-indexed types, and to provide a theory of indexed programming which is general enough to both describe type- and term-indexed programming and prescribe approaches to programming with more general forms of indexing. This will be achieved by considering specific problems in indexed programming (WP1 through WP4), as well as by developing a foundation for indexed programming based upon the categorical notion of a fibration (WP5). The application of categorical methods to functional programming has proven to be hugely successful over the years, so there is good reason to believe that our categorical methodology is appropriate for the proposed research.