Masters's Thesis: On the expressive power of effect handlers and monadic reflection
Author: Yannick Forster
Advisors: Dr. Ohad Kammar, Prof. Dr. Marcelo Fiore
Written at the University of Cambridge for an MPhil degree in Advanced Computer Science
Effect handlers and monadic reflection are both programming paradigms for implementing computational effects such as exceptions or I/O.
In this thesis we compare the expressive power of effect handlers and monadic reflection.
This comparison is based on two core calculi λ_eff, introduced by Kammar, Lindley and Oury and λ_mon, introduced by Filinski, both being extensions of Levy's call-by-push-value calculus.
We prove adequacy of the set-theoretic dentotational semantics of λ_eff.
We give a finite, adequate set-theoretic semantics for λ_mon, define the notion of typed and untyped macro expressability following Felleisen and show that there is a macro translation from λ_mon to untyped λ_eff, but no translation from λ_eff to typed λ_mon.
- Slides from thesis presentation: Slides
- More detailed slides from qualifying exam: Slides
- Submitted thesis: Thesis