Effects and algebraic theories.

点击翻译按钮获取中文摘要

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.