Relational reasoning for effects and handlers

Abstract

This thesis studies relational reasoning techniques for FRANK, a strict functional language supporting algebraic effects and their handlers, within a general, formalised approach for completely characterising observational equivalence. Algebraic effects and handlers are an emerging paradigm for representing computational effects where primitive operations, which give rise to an effect, are primary, and given semantics through their interpretation by effect handlers. FRANK is a novel point in the design space because it recasts effect handling as part of a generalisation of call-by-value function application. Furthermore, FRANK generalises unary effect handlers to the n-ary notion of multihandlers, supporting more elegant expression of certain handlers. There have been recent efforts to develop sound reasoning principles, with respect to observational equivalence, for languages supporting effects and handlers. Such techniques support powerful equational reasoning about code, such as substitution of equivalent sub-terms (‘equals for equals’) in larger programs. However, few studies have considered a complete characterisation of observational equivalence, and its implications for reasoning techniques. Furthermore, there has been no account of reasoning principles for FRANK programs. Our first contribution is a formal reconstruction of a general proof technique, triangulation, for proving completeness results for observational equivalence. The technique brackets observational equivalence between two structural relations, a logical and an applicative notion. We demonstrate the triangulation proof method for a pure simply-typed λ-calculus. We show that such results are readily formalisable in an implementation of type theory, specifically AGDA, using state-of-the-art technology for dealing with syntaxes with binding. Our second contribution is a calculus, ELLA, capturing the essence of FRANK’s novel design. In particular, ELLA supports binary handlers and generalises function application to incorporate effect handling. We extend our triangulation proof technique to this new setting, completely characterising observational equivalence for this calculus. We report on our partial progress in formalising our extension to ELLA in AGDA. Our final contribution is the application of sound reasoning principles, inspired by existing literature, to a variety of ELLA programs, including a proof of associativity for a canonical pipe multihandler. Moreover, we show how leveraging completeness leads, in certain instances, to simpler proofs of observational equivalence.