Categorical Foundations for Indexed Programming

类型系统已经成为编程语言设计和实现的一个组成部分，在安全性、数据库、并发和分布式编程等领域做出了重要贡献。类型系统提供的信息可用于诸如错误检测、程序优化和内存管理等任务。类型系统管理编程语言对值和表达式的数据类型分类，这决定了如何操作这些类型的数据以及这些数据如何交互。最初，类型系统只包含简单的数据类型，如Int和Char，用于对整数和字符等基本数据进行分类。然而，高级类型系统支持复杂的类型，这些类型不仅可以保证类型良好的程序没有简单的错误，比如试图添加非数字表达式，而且还可以保证它们保留不变量，不违反空间或其他约束，可以按原则进行优化，或者满足其他复杂的正确性属性。类型系统研究的大部分努力都是为了缩小程序员对计算实体的了解与类型可以表达它们之间的语义差距。增加类型系统的表达能力和推理能力的最有希望的方法之一是允许通过其他信息对类型进行索引。例如，与其简单地使用类型List表示列表数据类型，还可以通过附加信息对列表类型进行索引，这些信息可用于检测更多错误、执行更多优化，并提供更好的正确性保证。因此，索引中的额外信息有助于缩小前面提到的语义差距。索引编程是使用索引类型进行编程的实践。也许最常见的索引形式是通过其他类型对类型进行索引。例如，要对整数列表或布尔值列表或类型为t的数据列表的列表进行建模，可以使用类型索引类型，如List Int或List Bool或List （List t）。最近，开发了一些编程语言，不仅可以通过其他类型，还可以通过术语对类型进行索引。例如，要对长度为3的列表或特定证明p证明的列表进行排序，可以使用诸如List 3或List p这样的术语索引类型。索引编程的实践现在已经发展到需要有原则的基础来进一步发展这个主题的阶段。提出研究的目的是发展索引规划的分类基础。也就是说，它旨在提高对涉及传统术语索引和类型索引类型的特定问题的理解和解决问题的能力，并提供索引编程的理论，该理论足够通用，既可以描述类型索引和术语索引编程，也可以规定使用更通用的索引形式进行编程的方法。这将通过考虑索引规划（WP1到WP4）中的特定问题，以及基于纤维的分类概念（WP5）开发索引规划的基础来实现。多年来，分类方法在函数式编程中的应用已被证明是非常成功的，因此有充分的理由相信我们的分类方法适用于所提出的研究。

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.