[Supporting material] On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control

We compare the expressive power of three programming abstractions
for user-defined computational effects: Bauer and Pretnar's effect
handlers, Filinski's monadic reflection, and delimited control
without answer-type-modification. This comparison allows a precise
discussion about the relative expressiveness of each programming
abstraction. It also demonstrates the sensitivity of the relative
expressiveness of user-defined effects to seemingly orthogonal
language features.<br><br>

We present three calculi, one per abstraction, extending Levy's
call-by-push-value. For each calculus, we present syntax,
operational semantics, a natural type-and-effect system, and, for
effect handlers and monadic reflection, a set-theoretic denotational
semantics. We establish their basic metatheoretic properties:
safety, termination, and, where applicable, soundness and
adequacy. Using Felleisen's notion of a macro translation, we show
that these abstractions can macro-express each other, and show which
translations preserve typeability. We use the adequate finitary
set-theoretic denotational semantics for the monadic calculus to
show that effect handlers cannot be macro-expressed while preserving
typeability either by monadic reflection or by delimited control.
Our argument fails with simple changes to the type system such as
polymorphism and inductive types. We supplement our development with
a mechanised Abella formalisation.