Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Abstracting Effect Systems for Algebraic Effect Handlers

Takuma Yoshioka, Taro Sekiyama, Atsushi Igarashi

TL;DR

This work introduces λ_EA, a calculus whose effect system is parameterized by abstract effect algebras to unify and reason about diverse representations of effect collections in algebraic effects. By defining safety conditions on algebras, it proves type-and-effect safety for any instantiated instance, and demonstrates expressiveness by modeling set-based and row-based systems (sets, simple rows, scoped rows) and a novel multisets representation. The framework is extended with lift coercions and type-erasure semantics, each with dedicated safety requirements, and the authors show how translations from existing systems preserve typing, validating λ_EA as a safe, modular intermediate language. Extensions and comparisons to future-proof the theory include handling mechanisms, unification/type inference, constrained collections, and implementation strategies for practical language support.

Abstract

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 ${λ_{\mathrm{EA}}}$ equipped with an effect system that abstracts the existing effect systems for algebraic effect handlers. The effect system of ${λ_{\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 ${λ_{\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 ${λ_{\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.

Abstracting Effect Systems for Algebraic Effect Handlers

TL;DR

This work introduces λ_EA, a calculus whose effect system is parameterized by abstract effect algebras to unify and reason about diverse representations of effect collections in algebraic effects. By defining safety conditions on algebras, it proves type-and-effect safety for any instantiated instance, and demonstrates expressiveness by modeling set-based and row-based systems (sets, simple rows, scoped rows) and a novel multisets representation. The framework is extended with lift coercions and type-erasure semantics, each with dedicated safety requirements, and the authors show how translations from existing systems preserve typing, validating λ_EA as a safe, modular intermediate language. Extensions and comparisons to future-proof the theory include handling mechanisms, unification/type inference, constrained collections, and implementation strategies for practical language support.

Abstract

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 equipped with an effect system that abstracts the existing effect systems for algebraic effect handlers. The effect system of 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 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 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.
Paper Structure (46 sections, 13 theorems, 18 equations, 7 figures, 2 tables)

This paper contains 46 sections, 13 theorems, 18 equations, 7 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background: Effect Systems for Algebraic Effect Handlers
  3. Our Work
  4. Overview
  5. Review: Algebraic Effects and Handlers
  6. Effect Systems for Algebraic Effects and Handlers
  7. A Role of Effect Systems
  8. Set-Based Effect Systems
  9. Row-Based Effect Systems
  10. Our Work: Abstracting Effect Systems
  11. Abstracting Effects
  12. Syntax
  13. Kind System
  14. Effect Algebras
  15. $\lambda_{\mathrm{EA}}$: A Calculus with Abstract Effect System
  16. ...and 31 more sections

Key Result

Lemma 5.4

If $\emptyset \vdash \mathit{e} : \mathit{A} \mid \varepsilon$ and $\mathit{e} \longrightarrow ^ * \mathit{e'} \centernot \longrightarrow$, then one of the following holds:

Figures (7)

  • Figure 1: Typelike syntax over an label signature $\Sigma_{\mathrm{lab}}$ and an effect signature $\Sigma_{\mathrm{eff}}$.
  • Figure 2: Kinding rules.
  • Figure 3: Program syntax of $\lambda_{\mathrm{EA}}$.
  • Figure 4: Operational semantics of $\lambda_{\mathrm{EA}}$.
  • Figure 5: Type-and-effect system of $\lambda_{\mathrm{EA}}$.
  • ...and 2 more figures

Theorems & Definitions (30)

  • Definition 3.1: Signatures
  • Example 3.2: Label Signatures of $\mathsf{Exc}$ and $\mathsf{State}$
  • Example 3.3: Effect Signature of Effect Sets
  • Definition 3.4: Well-Formedness-Preserving Functions
  • Definition 3.5: Effect algebras
  • Example 3.6: Effect Sets
  • Example 3.7: Simple Rows
  • Example 3.8: Scoped Rows
  • Definition 5.1: Safety Conditions
  • Example 5.2: Unsafe Effect Algebras
  • ...and 20 more