Abstracting Effect Systems for Algebraic Effect Handlers

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 <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:msub> <mml:mi>λ</mml:mi> <mml:mi fontfamily="Georgia" mathvariant="normal">EA</mml:mi> </mml:msub> </mml:math> equipped with an effect system that abstracts the existing effect systems for algebraic effect handlers. The effect system of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:msub> <mml:mi>λ</mml:mi> <mml:mi>EA</mml:mi> </mml:msub> </mml:math> 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 <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:msub> <mml:mi>λ</mml:mi> <mml:mi>EA</mml:mi> </mml:msub> </mml:math> 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 <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:msub> <mml:mi>λ</mml:mi> <mml:mi>EA</mml:mi> </mml:msub> </mml:math> 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.