Effects and algebraic theories.

这个项目属于EPSRC信息和通信技术(ICT)的研究主题。这个项目涉及编程语言的基础、它们的语义和类型系统。计算效果是表示不纯行为的编程语言的一个特征，例如输入和输出操作、异常、状态、不确定性。这些操作在实际编程中被广泛使用，并由许多编程语言提供。然而，它们的数学基础还没有得到充分的探索。在他有影响力的著作中，莫吉给出了使用单数的计算效果的一般指称语义。他的想法随后被Haskell用纯函数式语言实现，其中Monad被用来模拟副作用。普洛特金和鲍尔引入了代数效应的概念，这是一种计算效应的特殊方法，其中不纯行为是由一组运算产生的。这些运算的性质是由方程式指定的，这使得将代数效应表示为传统上在通用代数中研究的代数理论成为可能。每个代数理论都会产生一个单数，从而与莫吉的语义有联系。为了解释效应，人们提出了对一阶代数理论的各种扩展。例子包括由Staton提出的参数化代数理论，以及由Fiore、Hur和Mahmoud发展的二阶代数理论。Fiore和Staton分别使用替换代数和右Lambda代数这两个二阶代数理论的特例来模拟跳跃效应和涉及代码指针堆栈的计算，进一步探索效应和二阶代数理论之间的联系是我将要追求的一个很有前途的研究方向。我们的目标是找到其他能够产生效应的代数理论，反之亦然。首先，这种方法将导致更好地理解效果的语义。从长远来看，效应和代数之间的联系可以为用计算效应扩展编程演算提供一个通用的框架。然后，可以在高级通用编程语言之上实现这些扩展。在信通技术研究主题中，该项目是理论计算机科学领域的一部分，因为它采用了形式推理、逻辑概念和语义学。该项目也是编程语言和编译器领域的一部分，因为它的目标是更好地理解编程语言，并可能导致新的实现。

This project falls within the EPSRC Information and communication technologies (ICT) research theme.This project is concerned with the foundations of programming languages, their semantics and type systems. Computational effects are a feature of programming languages representing impure behaviour, such as input and output operations, exceptions, state, nondeterminism. These operations are widely used in practical programming and are provided by many programming languages. However, their mathematical foundations have not been fully explored yet.In his influential work, Moggi gives a general denotational semantics for computational effects using monads. His idea was subsequently implemented in the pure functional language by Haskell, where monads are used to simulate side effects. Plotkin and Power introduce the idea of algebraic effects, a particular approach to computational effects where the impure behaviour results from a set of operations. The properties of these operations are specified by equations, making it possible to present algebraic effects as algebraic theories, traditionally studied in universal algebra. Each algebraic theory gives rise to a monad, thus exhibiting the connection with Moggi's semantics.In order to interpret effects, various extensions of first-order algebraic theories have been proposed. Examples include parameterised algebraic theories, proposed by Staton, and second-order algebraic theories developed by Fiore, Hur and Mahmoud. Fiore and Staton use substitution algebras and right lambda algebras, particular instances of second-order algebraic theories, to model jump effects and computation involving stacks of code pointers, respectively.Exploring further the connection between effects and second-order algebraic theories is a promising research direction that I will pursue. The goal is to find other algebraic theories that give rise to effects and vice-versa. In the first instance, this approach will lead to a better understanding of the semantics of effects. In the long term, the connection between effects and algebra could provide a general framework for extending programming calculi with computational effects. These extensions could then be implemented on top of high-level general-purpose programming languages. Within the ICT research theme, this project is part of the Theoretical Computer Science area because it employs formal reasoning, logical concepts and semantics. The project is also part of the Programming languages and compilers area since its aim is to understand programming languages better, and may lead to new implementations.