Many effect systems for algebraic effect handlers are designed to guarantee that all invoked effects are handled adequately. However, respective researchers have developed their own effect systems that differ in how to represent the collections of effects that may happen. This situation results in blurring what is required for the representation and manipulation of effect collections in a safe effect system. In this work, we present a language ${\lambda_{\mathrm{EA}}}$ equipped with an effect system that abstracts the existing effect systems for algebraic effect handlers. The effect system of ${\lambda_{\mathrm{EA}}}$ is parameterized over effect algebras, which abstract the representation and manipulation of effect collections in safe effect systems. We prove the type-and-effect safety of ${\lambda_{\mathrm{EA}}}$ by assuming that a given effect algebra meets certain properties called safety conditions. As a result, we can obtain the safety properties of a concrete effect system by proving that an effect algebra corresponding to the concrete system meets the safety conditions. We also show that effect algebras meeting the safety conditions are expressive enough to accommodate some existing effect systems, each of which represents effect collections in a different style. Our framework can also differentiate the safety aspects of the effect collections of the existing effect systems. To this end, we extend ${\lambda_{\mathrm{EA}}}$ and the safety conditions to lift coercions and type-erasure semantics, propose other effect algebras including ones for which no effect system has been studied in the literature, and compare which effect algebra is safe and which is not for the extensions.

翻译：许多针对代数效应处理器的效应系统旨在保证所有被调用的效应都能被妥善处理。然而，不同研究者开发的效应系统在表示可能发生的效应集合方式上存在差异。这导致一个核心问题：安全效应系统中效应集合的表示与操作究竟需要满足哪些必要条件？本文提出了一种配备效应系统的语言${\lambda_{\mathrm{EA}}}$，该语言对现有代数效应处理器的效应系统进行了抽象化。${\lambda_{\mathrm{EA}}}$的效应系统以效应代数为参数，这些代数抽象了安全效应系统中效应集合的表示与操作。通过假设给定效应代数满足称为安全条件的特定属性，我们证明了${\lambda_{\mathrm{EA}}}$的类型与效应安全性。由此，通过证明具体效应系统对应的效应代数满足安全条件，即可获得该系统的安全特性。我们还表明，满足安全条件的效应代数具有足够的表达能力，能够容纳现有若干采用不同方式表示效应集合的效应系统。该框架还能区分现有效应系统中效应集合安全性的不同层面。为此，我们扩展了${\lambda_{\mathrm{EA}}}$及安全条件以支持类型强制转换和类型擦除语义，提出了文献中尚未系统研究的新型效应代数，并针对扩展情况比较了各效应代数的安全性。