Algebraic Computational Effects in 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.