Algebraic effects & handlers are a modular approach for modeling side-effects in functional programming. Their syntax is defined in terms of a signature of effectful operations, encoded as a functor, that are plugged into the free monad; their denotational semantics is defined by fold-style handlers that only interpret their part of the syntax and forward the rest. However, not all effects are algebraic: some need to access an internal computation. For example, scoped effects distinguish between a computation in scope and out of scope; parallel effects parallellize over a computation, latent effects defer a computation. Separate definitions have been proposed for these higher-order effects and their corresponding handlers, often leading to expedient and complex monad definitions. In this work we propose a generic framework for higher-order effects, generalizing algebraic effects & handlers: a generic free monad with higher-order effect signatures and a corresponding interpreter. Specializing this higher-order syntax leads to various definitions of previously defined (scoped, parallel, latent) and novel (writer, bracketing) effects. Furthermore, we formally show our framework theoretically correct, also putting different effect instances on formal footing; a significant contribution for parallel, latent, writer and bracketing effects.

翻译：代数效应与处理器是函数式编程中处理副作用的一种模块化方法。其语法由作为函子编码的有效操作签名定义，这些签名被嵌入自由单子中；其指称语义通过折叠式处理器实现，该处理器仅解释语法中自身对应的部分，并将剩余部分转发。然而，并非所有效应都是代数的：部分效应需要访问内部计算。例如，作用域效应需区分作用域内外的计算；并行效应对计算进行并行化处理；延迟效应则推迟计算。针对这些高阶效应及其对应的处理器，现有研究分别提出了不同的定义，往往导致单子定义变得冗长复杂。本文提出一个泛化代数效应与处理器的高阶效应通用框架：通过高阶效应签名构建泛型自由单子，并设计相应的解释器。通过特化该高阶语法，我们不仅重新定义了先前提出的（作用域、并行、延迟）效应，还定义了新型（写入器、括号化）效应。此外，我们从理论上严格证明了该框架的正确性，同时为不同效应实例建立了形式化基础——这对并行、延迟、写入器和括号化效应而言，是一项重要贡献。