Foundations for programming and implementing effect handlers

NOTE I have made a draft copy of the dissertation available in this repository. I ask that you do not link to or distribute the draft anywhere, because I will delete the file once the final revision has been submitted after the viva. I will make the final revision publicly available at a stable link.

---

Submitted May 30, 2021. Viva August 13, 2021.

The board of examiners consists of

• Andrew Kennedy (Facebook London)
• Edwin Brady (University of St Andrews)
• Ohad Kammar (The University of Edinburgh)
• Stephen Gilmore (The University of Edinburgh)

Thesis structure

The dissertation is structured as follows.

Introduction

• Chapter 1 puts forth an argument for why effect handlers matter. Following this argument it provides a basic introduction to several different approaches to effectful programming through the lens of the state effect. In addition, it also declares the scope and contributions of the dissertation, and discusses some related work.

Background

• Chapter 2 defines some basic mathematical notation and constructions that are they pervasively throughout this dissertation.

• Chapter 3 presents a literature survey of continuations and first-class control. I classify continuations according to their operational behaviour and provide an overview of the various first-class sequential control operators that appear in the literature. The application spectrum of continuations is discussed as well as implementation strategies for first-class control.

Programming

• Chapter 4 introduces a polymorphic fine-grain call-by-value core calculus, λ_b, which makes key use of Remy-style row polymorphism to implement polymorphic variants, structural records, and a structural effect system. The calculus distils the essence of the core of the Links programming language.

• Chapter 5 presents three extensions of λ_b, which are λ_h that adds deep handlers, λ^† that adds shallow handlers, and λ^‡ that adds parameterised handlers. The chapter also contains a running case study that demonstrates effect handler oriented programming in practice by implementing a small operating system dubbed Tiny UNIX based on Ritchie and Thompson's original UNIX.

Implementation

• Chapter 6 develops a higher-order continuation passing style translation for effect handlers through a series of step-wise refinements of an initial standard continuation passing style translation for λ_b. Each refinement slightly modifies the notion of continuation employed by the translation. The development ultimately leads to the key invention of generalised continuation, which is used to give a continuation passing style semantics to deep, shallow, and parameterised handlers.

• Chapter 7 demonstrates an application of generalised continuations to abstract machine as we plug generalised continuations into Felleisen and Friedman's CEK machine to obtain an adequate abstract runtime with simultaneous support for deep, shallow, and parameterised handlers.

Expressiveness

• Chapter 8 shows that deep, shallow, and parameterised notions of handlers can simulate one another up to specific notions of administrative reduction.

• Chapter 9 studies the fundamental efficiency of effect handlers. In this chapter, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. Specifically, we consider the generic count problem using a pure PCF-like base language λ_b^→ (a simply typed variation of λ_b) and its extension with effect handlers λ_h^→. We show that λ_h^→ admits an asymptotically more efficient implementation of generic count than any λ_b^→ implementation.

Conclusions

• Chapter 10 concludes and discusses future work.

Appendices

• Appendix A contains a proof that shows the Get-get equation for state is redundant.
• Appendix B contains the proof details for the higher-order uncurried CPS translation for deep and shallow handlers.
• Appendix C contains the proof details and gadgetry for the complexity of the effectful generic count program.
• Appendix D provides a sample implementation of the Berger count program and discusses it in more detail.

Building

To build the dissertation you need the Informatics thesis LaTeX class with the University of Edinburgh crests. Invoking make on the command line ought to produce a PDF copy of the dissertation named thesis.pdf, e.g.

$ make