Algebraic Computational Effects in Programming Languages

编程语言中的代数计算效应

• 批准号: 2495799
• 金额: --
• 依托单位: University of Cambridge
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2495799
• 关键词: Algebraic; Computational; Effects; Programming; Languages

This research project's interests lie at the intersection of mathematics and computer science. It focuses on the interplay between mathematical formalism and programming languages.A significant success in semantics is the connection between the theory of universal algebra and the study of syntax without bound variables and its transformations. This, however, is limited to first-order languages, i.e. those without variable binding. If we want to move into more common and interesting languages, more complex mathematical theories are needed.To tackle this problem, Marcelo Fiore and Ola Mahmoud introduced second-order algebraic theories in their 2013 paper. In later work Fiore showed how control flow effects can be expressed in these algebraic theories. These include jumps between points in the program, and coroutines, functions that do not need to return to the same place that invoked them.Another class of algebras, one which may be called linear, though not in the sense of vector spaces, has found applications in expressing the notion of computational resources and event structures, which model causal links between events. It might be possible to use them to formalise the notion of ownership of data central to the design of the Rust programming language.Both of those, universal algebra, including the extension with second-order theories, and linear algebra make heavy use of category theory and can be alternatively called cartesian and monoidal algebras respectively, from cartesian and monoidal categories they connect to.I aim to investigate these algebraic approaches to expressing various effects in more depth. One interesting problem is that of determining what other common effects are and are not expressible in this framework. Of particular interest is the notion of concurrency, where programs can execute non-deterministically, and reflexivity, where programs create new code while executing. Another open question is that of generality. That is, having seen these algebras and the way they represent program features, can we find a way to unify them as instances of a more general mathematical framework.More broadly, while each of the areas of formalising behaviour of substitution, categorical semantics, algebraic effects and dependent type systems has been studied on its own, there is little work combining all of them and there is evidence that nontrivial issues arise in such attempts.

这个研究项目的兴趣在于数学和计算机科学的交叉点。它关注数学形式主义和程序设计语言之间的相互作用。语义学的一个重大成功是将泛代数理论与无约束变量语法及其变换的研究联系起来。然而，这仅限于一阶语言，即那些没有变量绑定的语言。如果我们想使用更常见和有趣的语言，就需要更复杂的数学理论。为了解决这个问题，Marcelo Fiore和奥拉马哈茂德在他们2013年的论文中引入了二阶代数理论。在后来的工作菲奥雷表明如何控制流的影响可以表示在这些代数理论。这些包括程序中点之间的跳转，以及协程，这些函数不需要返回到调用它们的相同位置。另一类代数，可以被称为线性代数，尽管不是向量空间的意义，已经在表达计算资源和事件结构的概念中找到了应用，这些概念模拟了事件之间的因果关系。也许可以使用它们来形式化Rust编程语言设计中核心的数据所有权概念。这两种代数，泛代数，包括二阶理论的扩展，和线性代数都大量使用了范畴理论，可以分别称为carnival和monoidal代数，我的目标是更深入地研究这些代数方法来表达各种效果。一个有趣的问题是，确定其他共同的影响是和不是在这个框架中表达。特别感兴趣的是并发性的概念，其中程序可以非确定性地执行，以及自反性，其中程序在执行时创建新代码。另一个悬而未决的问题是普遍性问题。也就是说，在看到这些代数和它们表示程序特征的方式之后，我们是否可以找到一种方法来将它们统一为更一般的数学框架的实例。更广泛地说，虽然替代、范畴语义、代数效果和依赖类型系统的形式化行为的每一个领域都被单独研究过，几乎没有将所有这些方法结合起来的工作，有证据表明，在这种尝试中出现了一些重要的问题。