Relational reasoning for effects and handlers
View/ Open
Date
25/07/2020Author
McLaughlin, Craig
Metadata
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.