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

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，用于分类基本数据，如整数和字符。然而，高级类型系统支持复杂的类型，不仅可以保证良好类型的程序没有简单的错误，例如试图添加非数值表达式，而且还可以保证它们保持不变，不违反空间或其他约束，可以以原则性的方式进行优化，或者满足其他复杂的正确性属性。类型系统研究的大部分努力都是为了缩小程序员对计算实体的了解和类型可以表达它们之间的语义差距。增加类型系统的表达能力和推理能力的最有希望的方法之一是允许类型被其他信息索引。例如，不是简单地具有表示列表数据类型的类型List，而是列表类型可以通过附加信息来索引，这些附加信息可以用于检测更多错误，执行更多优化，并提供比其他方式更大的正确性保证。因此，索引中的额外信息有助于缩小上述语义差距。索引编程是使用索引类型进行编程的实践。也许最常见的索引形式是通过其他类型来索引类型。例如，为了对类型t的整数列表或布尔列表或数据列表的列表建模，可以使用类型索引类型，例如List Int或List Bool或List（List t）。最近，编程语言已经开发出允许类型不仅通过其他类型索引，而且还通过术语索引。例如，要对长度为3的列表或特定证明p证明排序的列表进行建模，可以使用诸如List 3或List p之类的术语索引类型。索引编程的实践现在已经发展到需要有原则性基础才能进一步发展的阶段。建议的研究的目的是开发一个分类的基础索引编程。也就是说，它的目的是提高理解和解决涉及传统的术语索引和类型索引类型的特定问题的能力，并提供一个索引编程的理论，该理论足够通用，可以描述类型和术语索引编程，并规定使用更通用的索引形式编程的方法。这将通过考虑索引编程（WP 1到WP 4）中的特定问题以及基于纤维化的分类概念（WP 5）开发索引编程的基础来实现。多年来，分类方法在函数式编程中的应用已被证明是非常成功的，因此有充分的理由相信我们的分类方法适用于所提出的研究。

项目成果

Abstraction and invariance for algebraically indexed types

代数索引类型的抽象和不变性

• DOI: 10.1145/2429069.2429082
• 发表时间: 2013
• 作者: Atkey R

Amortised Resource Analysis with Separation Logic

具有分离逻辑的摊销资源分析

• DOI: 10.2168/lmcs-7(2:17)2011
• 发表时间: 2011
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Atkey R

Foundations of Software Science and Computational Structures

软件科学和计算结构基础

• DOI: 10.1007/978-3-642-19805-2_3
• 发表时间: 2011
• 作者: Levy P