Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Rows and Capabilities as Modal Effects

Wenhao Tang, Sam Lindley

TL;DR

The paper tackles the challenge of comparing and combining diverse effect systems rooted in rows and capabilities. It introduces Met(X), a modal, System F-style core that decouples effect tracking from functions, parameterized by an abstract effect structure X. Through macro-encodings, it shows that both row-based (e.g., F^ε) and capability-based (e.g., Effekt/System C) systems can be faithfully represented in Met(X), preserving typing and semantics and enabling direct comparison of their tracking mechanisms. The contributions include a formal core calculus, modality-based extensions (local labels and modality-parameterised handlers), and detailed encodings of concrete systems with proofs of soundness. Together, these results offer a uniform intermediate representation for designing, optimizing, and extending effect systems across language paradigms, with practical guidance for language designers.

Abstract

Effect handlers allow programmers to model and compose computational effects modularly. Effect systems statically guarantee that all effects are handled. Several recent practical effect systems are based on either row polymorphism or capabilities. However, there remains a gap in understanding the precise relationship between effect systems with such disparate foundations. The main difficulty is that in both row-based and capability-based systems, effect tracking is typically entangled with other features such as functions. We propose a uniform framework for encoding, analysing, and comparing effect systems. Our framework exploits and generalises modal effect types, a recent novel effect system which decouples effect tracking from functions via modalities. Modalities offer fine-grained control over when and how effects are tracked, enabling us to express different strategies for effect tracking. We give encodings as macro translations from existing row-based and capability-based effect systems into our framework and show that these encodings preserve types and semantics. Our encodings reveal the essence of effect tracking mechanisms in different effect systems, enable a direct analysis on their differences, and provide practical insights on language design.

Rows and Capabilities as Modal Effects

TL;DR

The paper tackles the challenge of comparing and combining diverse effect systems rooted in rows and capabilities. It introduces Met(X), a modal, System F-style core that decouples effect tracking from functions, parameterized by an abstract effect structure X. Through macro-encodings, it shows that both row-based (e.g., F^ε) and capability-based (e.g., Effekt/System C) systems can be faithfully represented in Met(X), preserving typing and semantics and enabling direct comparison of their tracking mechanisms. The contributions include a formal core calculus, modality-based extensions (local labels and modality-parameterised handlers), and detailed encodings of concrete systems with proofs of soundness. Together, these results offer a uniform intermediate representation for designing, optimizing, and extending effect systems across language paradigms, with practical guidance for language designers.

Abstract

Effect handlers allow programmers to model and compose computational effects modularly. Effect systems statically guarantee that all effects are handled. Several recent practical effect systems are based on either row polymorphism or capabilities. However, there remains a gap in understanding the precise relationship between effect systems with such disparate foundations. The main difficulty is that in both row-based and capability-based systems, effect tracking is typically entangled with other features such as functions. We propose a uniform framework for encoding, analysing, and comparing effect systems. Our framework exploits and generalises modal effect types, a recent novel effect system which decouples effect tracking from functions via modalities. Modalities offer fine-grained control over when and how effects are tracked, enabling us to express different strategies for effect tracking. We give encodings as macro translations from existing row-based and capability-based effect systems into our framework and show that these encodings preserve types and semantics. Our encodings reveal the essence of effect tracking mechanisms in different effect systems, enable a direct analysis on their differences, and provide practical insights on language design.

Paper Structure

This paper contains 79 sections, 42 theorems, 83 equations, 19 figures.

Table of Contents

  1. Introduction
  2. Overview
  3. Modal Effects and Met($\mathcal{X}$)
  4. Effect Contexts
  5. Absolute Modalities
  6. Relative Modalities
  7. Effect Structures
  8. Rows as Modal Effects
  9. Capabilities as Modal Effects
  10. First-Order Blocks
  11. Boxes
  12. Higher-Order Blocks
  13. Block Calls
  14. Comparing Rows and Capabilities
  15. Encoding Effect Handlers
  16. ...and 64 more sections

Key Result

theorem 1

In Met($\mathcal{X}$) where $\mathcal{X}$ satisfies the validity conditions, if $\,\Omega\mid\cdot \vdash M:A \;{\color{gray}{@}}\, {\color{dblue}{E}}$, then either $M\mid\Omega\mathrel{\leadsto} N\mid\Omega'$ for some $N$ and $\Omega'$, or $M$ is in a normal form with respect to $E$.

Figures (19)

  • Figure 1: Typing rules and auxiliary rules of Met($\mathcal{X}$).
  • Figure 2: Operational semantics of Met($\mathcal{X}$).
  • Figure 3: An encoding of System $\textsf{F}^{\epsilon}$ in Met(${\mathcal{R}_{\textsf{scp}}}$).
  • Figure 4: Syntax and typing rules for System C. We mostly follow the syntax of BrachthauserSLB22. The main difference is that we write $\Rightarrow$ for block types to emphasise they are second-class.
  • Figure 5: An encoding of System C in Met($\mathcal{S}$).
  • ...and 14 more figures

Theorems & Definitions (48)

  • definition 1: Effect structure
  • definition 2: Simple Rows
  • definition 3: Scoped Rows
  • definition 4: Sets
  • definition 5: Validity Conditions
  • definition 6: Normal Forms
  • theorem 1: Progress
  • theorem 2: Subject Reduction
  • theorem 3: Type Preservation
  • theorem 4: Semantics Preservation
  • ...and 38 more