Nowadays, computer systems control almost every aspect of our lives. There is a constantly increasing demand for safety-critical software of growing complexity. To meet this demand, one needs appropriate tools, and at the very heart of softwaredevelopment toolchain lays a programming language in which one can describe the logic of the system. The better the design of the language, the more flexible, reliable, and scalable the system can be.
Maciej Adam Pieróg
One of the goals of computer science as an academic discipline is to provide insights and ideas both for programming languages and tools to analyse programmes. For example, one of the most desirable features of a well-designed system is modularity: parts of the system are loosely coupled, and we strive for each component to be easy to understand on its own, with little knowledge about the details of the rest of the system. This makes the development process easier (since the programmer does not have to think about the entire system all the time, only about one particular part), and each component can be modified and tested in isolation. A well-designed programming language can make modularity more effortless to achieve. Moreover, new technologies, such as parallel and distributed computing, render some widely used programming techniques (such as imperative programming) obsolete. This creates new challenges for computer science to come up with new methodologies and tools.
One such methodology, which is not new, but gaining a lot of attention recently, is functional programming. Its strength lies in strong modularity features and precise, mathematical semantics, which makes functional programmes much easier to understand and reason about. Within the area of functional programming, a recent advancement has been made by the introduction of algebraic effects and their handlers. They allow the programmer to precisely control the behaviour of each part of the programme (both locally, in a small piece of code, and globally, specifying the relations between big components), giving the programmer both strong tools of expression, and a way to maintain modularity.
Algebraic effects and handlers are quite a recent addition to the area of programming and programming language research. They are very promising, and seem to be able to solve many practical and theoretical problems, but some aspects are still to be investigated, which was the topic of this project.
Specifically, the first task was to establish a precise relationship of algebraic effects with other features that allow structuring of programmes, that is, other approaches to computational effects. The goal of this task was to better understand which features are well-suited to be included in programming languages – we strive for languages that are simple and yet expressive. The obtained result was that algebraic effects are no less expressive than other features studied before, but have more practical, programmer-friendly angle.
Another task of the project was to come up with new programming constructs that allow the programmer to strengthen modularity and reason about programming with algebraic effects. One tangible result of this task is an implementation of an experimental programming language that provides the new modular features, and which has a novel formal calculus as its basis.
Finally, the project was concerned with algebraic specification of effects: giving the programmer and language designer some mathematical tools to specify and reason about programmes that use algebraic effects. We developed some new mathematical foundations for understanding the connection between the practice of defining algebraic effects in a programming language and their mathematical underpinning. One additional result is a system for automatic generation of correct-by-construction implementations of effects and their related algebraic specifications.
In general, the most attractive quality of algebraic effects is that the combine precise mathematical foundations with practical tools for programming and reasoning about programmes. The results of this project allowed to better understand algebraic effects, and solved some problems that had barred the way to their popular adoption in programming practice.
How did you benefit from the POLONEZ fellowship?
The greatest benefit by far was the means and opportunity to collaborate with people, both at Wrocław University and elsewhere. This allowed me to learn and expand my research area, leading to some quite exciting results. This was also quite an exciting period for me personally. In between the moment I applied for the scholarship and the conclusion of the project, my two children were born, and in that time I really did appreciate the support and flexibility I had thanks to the fellowship.
Dr Maciej Piróg graduated in computer science at the University of Wrocław. He obtained his PhD at the University of Oxford, where he also completed a postdoctoral training. He works on the theory and practice of programming languages. To learn more about Dr Piróg and his research interests, visit http://www.ii.uni.wroc.pl/~mpirog/
