Categorical Foundations for Indexed Programming

索引编程的分类基础

• 批准号: EP/G068917/1
• 负责人: Patricia Johann
• 金额: $ 35.92万
• 依托单位: University of Strathclyde
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2010
• 资助国家: 英国
• 起止时间: 2010 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FG068917%2F1
• 关键词: Categorical; Foundations; Indexed; Programming; Categorical; Foundations; 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.

类型系统已成为编程语言设计和实施的不可或缺的一部分，从而在安全性，数据库以及并发和分布式编程等领域做出了基本贡献。类型系统提供可用于错误检测，程序优化和内存管理等任务的信息。类型系统控制编程语言对数据类型的值和表达式的分类，这确定了如何操纵这些类型的数据以及这些数据如何相互作用。最初，类型系统仅包含简单数据类型，例如INT和CHAR，用于对基本数据（例如整数和字符）进行分类。但是，高级类型系统支持复杂的类型，这些类型不仅可以保证良好的程序没有简单的错误，例如试图添加非数字表达式，而且可以保留不变性，不违反空间或其他约束，也可以以原则性的方式进行优化，或者可以满足其他复杂的正确性。类型系统研究中的大部分努力旨在缩小程序员对计算实体的了解与它们可以表达的类型之间的语义差距。一种提高类型系统的表现力和推理能力的最有希望的方法之一是允许其他信息索引类型。例如，可以通过其他信息来索引列表类型，而不是简单地说出列表数据类型的类型列表，这些信息可用于检测更多的错误，执行更多优化，并提供比其他可能的更正确的正确性保证。因此，指数中的额外信息有助于缩小上述语义差距。索引编程是用索引类型进行编程的实践。索引的最常见形式可能是其他类型的索引类型。为了模型的整数列表或布尔值列表或T型数据列表的列表，例如，可以使用类型索引类型的类型，例如list int或list bool或list（列表t）。最近，已经开发了编程语言，这些语言允许类型不仅由其他类型索引，而且还可以用术语索引。例如，要使用特定证明P的长度3或列表进行模型列表，可以使用术语指数类型，例如列表3或列表P。索引编程的实践现已发展到需要原则上的基础以进一步采取主题的阶段。拟议的研究的目的是为索引编程的分类基础。也就是说，它旨在提高对涉及传统术语指数和类型索引类型的特定问题的理解和能力，并提供索引编程理论，该理论足以描述类型和项索引编程和规定以更一般形式的索引形式的编程方法和规定编程的方法。这将通过考虑索引编程中的特定问题（WP1至WP4），以及根据纤维的分类概念（WP5）开发索引编程的基础来实现。多年来，将分类方法应用于功能编程已取得了巨大成功，因此有充分的理由相信我们的分类方法适合拟议的研究。