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.

翻译：某些效应被认为比其他效应更高级。高阶效应提供了对编程概念的表达性强且简明的抽象，而低阶效应则允许对程序执行和资源进行更细粒度的控制。然而，通常我们希望使用高阶效应提供的便捷抽象来编写程序，同时仍从低阶效应所支持的优化中受益。一种解决方案是将高阶效应翻译为低阶效应。本文研究了代数效应与处理器如何使我们能够用低阶效应模拟高阶效应。具体而言，我们聚焦于状态与非确定性之间的交互——即Prolog所提供的局部状态。我们通过逐步映射将此高阶语义转化为一个低阶复合状态效应，类似于Prolog的沃伦抽象机所管理的效应。首先，我们给出从高阶局部状态语义到低阶全局状态语义的翻译，方法是在回溯时显式恢复状态更新。接着，我们完全消除非确定性，转而使用一个包含选择点栈的低阶状态。然后，我们通过限制自己仅进行增量式、可逆的状态更新来避免复制状态。我们展示了这些更新如何借助另一个状态效应存储在踪迹栈上。我们通过程序演算证明了所有步骤的正确性，其中效应处理器的融合律发挥了核心作用。