  Some effects are considered to be higher-level than others. High-level
effects provide expressive and succinct abstraction of programming concepts,
while low-level effects allow more fine-grained control over program execution
and resources. Yet, often it is desirable to write programs using the
convenient abstraction offered by high-level effects, and meanwhile still
benefit from the optimisations enabled by low-level effects. One solution is to
translate high-level effects to low-level ones.
  This paper studies how algebraic effects and handlers allow us to simulate
high-level effects in terms of low-level effects. In particular, we focus on
the interaction between state and nondeterminism known as the local state, as
provided by Prolog. We map this high-level semantics in successive steps onto a
low-level composite state effect, similar to that managed by Prolog's Warren
Abstract Machine. We first give a translation from the high-level local-state
semantics to the low-level global-state semantics, by explicitly restoring
state updates on backtracking. Next, we eliminate nondeterminsm altogether in
favor of a lower-level state containing a choicepoint stack. Then we avoid
copying the state by restricting ourselves to incremental, reversible state
updates. We show how these updates can be stored on a trail stack with another
state effect. We prove the correctness of all our steps using program
calculation where the fusion laws of effect handlers play a central role.
