Thesis

Alef: A bidirectional effect system for algebraic effects.

Abstract

The theory of algebraic effects and handlers has proven to be both a solid foundation for mathematical modelling of computational effects and a practical framework for the design of programming languages with effect systems. However, it is often the case that in the transition from theory to application much of the former’s conceptual clarity is lost. The main reason for this is that the abstract descriptions of even the most basic type-and-effect systems usually do not allow for direct implementations. In consequence, most languages with effect systems based on algebraic effects have complex implementations that rely on mechanisms not accounted for in the system’s formal description. This not only limits their extensibility but it may also hinder reasoning over concrete effectful programs.

For this thesis, we set out to formulate a simple algorithmic type-and-effect system for a core calculus with algebraic effects and handlers that we called Alef. By keeping the system’s formal description conceptually similar to well-known declarative presentations of effect systems, the task of extending the resulting implementation for it to support more advanced features should be straightforward.

Full text (in Spanish)

You can find the thesis in full here.