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，用于对整数和字符等基本数据进行分类。然而，高级类型系统支持复杂类型，这些复杂类型不仅可以保证好类型的程序没有简单的错误，例如尝试添加非数值表达式，还可以保证它们保留不变量，不违反空格或其他约束，可以按原则优化，或者满足其他复杂的正确性属性。类型系统研究的大部分工作旨在弥合程序员对计算实体的了解和类型对它们的表达之间的语义鸿沟。提高类型系统的表达能力和推理能力的最有前途的方法之一是允许其他信息对类型进行索引。例如，不是简单地让类型列表表示列表数据类型，而是可以通过附加信息来索引列表类型，这些附加信息可以用来检测更多错误、执行更多优化并提供比否则可能的更大的正确性保证。因此，索引中的额外信息有助于缩小上述语义鸿沟。索引编程是使用索引类型进行编程的实践。也许最常见的索引形式是按其他类型对类型进行索引。例如，为了对整数列表或布尔列表或类型t的数据列表的列表进行建模，可以使用类型索引类型，例如List Int或List Bool或List(List T)。最近，开发了编程语言，不仅允许按其他类型索引类型，而且还允许按术语索引类型。例如，为了对长度为3的列表或特定证明p所证明的列表进行建模，可以使用诸如列表3或列表p之类的术语索引类型。编入索引的方案编制做法现已发展到需要有原则的基金会才能进一步推动这一主题的阶段。拟议研究的目的是发展索引规划的范畴基础。也就是说，它的目的是提高对涉及传统术语索引和类型索引类型的具体问题的理解和解决具体问题的能力，并提供一种索引编程理论，该理论足够通用，以描述类型索引编程和术语索引编程，并规定具有更一般索引形式的编程方法。这将通过考虑编入索引的方案编制中的具体问题(WP1至WP4)以及为基于分类概念的编入索引的方案编制建立基础(WP5)来实现。多年来，将范畴方法应用于函数式编程已被证明是非常成功的，因此有充分的理由相信我们的范畴方法适合拟议的研究。

项目成果

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