Rows and Capabilities as Modal Effects

TL;DR

This paper introduces a unified framework using modal effect types to analyze, compare, and encode effect systems based on rows and capabilities, clarifying their relationships and guiding language design.

Contribution

It proposes a general modal effect type framework that decouples effect tracking from functions and provides encodings for existing effect systems, revealing their core mechanisms.

Findings

Encodings preserve types and semantics.

Framework clarifies differences between effect systems.

Provides practical insights for language design.

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.