Algebraic Computational Effects in Programming Languages

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

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.