Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Modal Effect Types

Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, Anton Lorenzen

TL;DR

This work introduces Modal Effect Types (Met), a robust framework for effectful programming that eliminates the need for explicit effect polymorphism by tracking ambient effect contexts as modalities. Built on multimodal type theory, Met distinguishes absolute $[E]$ and relative $<L|D>$ modalities to manage how effect contexts change across computations, handlers, and masking. The paper defines a core calculus Met, proves type soundness and effect safety, and shows how to encode traditional row-based effect polymorphism within Met and its surface language Metl. Extensions to data types, polymorphism, and richer handlers demonstrate practical scalability, and a detailed comparison with Koka and Effekt highlights the practical advantages of modal effect types for modular, first-class effects. The work lays groundwork for future language integrations (e.g., OCaml) and offers a principled approach to robustly managing effects without pervasive annotation overhead.

Abstract

Effect handlers are a powerful abstraction for defining, customising, and composing computational effects. Statically ensuring that all effect operations are handled requires some form of effect system, but using a traditional effect system would require adding extensive effect annotations to the millions of lines of existing code in these languages. Recent proposals seek to address this problem by removing the need for explicit effect polymorphism. However, they typically rely on fragile syntactic mechanisms or on introducing a separate notion of second-class function. We introduce a novel approach based on modal effect types.

Modal Effect Types

TL;DR

This work introduces Modal Effect Types (Met), a robust framework for effectful programming that eliminates the need for explicit effect polymorphism by tracking ambient effect contexts as modalities. Built on multimodal type theory, Met distinguishes absolute and relative modalities to manage how effect contexts change across computations, handlers, and masking. The paper defines a core calculus Met, proves type soundness and effect safety, and shows how to encode traditional row-based effect polymorphism within Met and its surface language Metl. Extensions to data types, polymorphism, and richer handlers demonstrate practical scalability, and a detailed comparison with Koka and Effekt highlights the practical advantages of modal effect types for modular, first-class effects. The work lays groundwork for future language integrations (e.g., OCaml) and offers a principled approach to robustly managing effects without pervasive annotation overhead.

Abstract

Effect handlers are a powerful abstraction for defining, customising, and composing computational effects. Statically ensuring that all effect operations are handled requires some form of effect system, but using a traditional effect system would require adding extensive effect annotations to the millions of lines of existing code in these languages. Recent proposals seek to address this problem by removing the need for explicit effect polymorphism. However, they typically rely on fragile syntactic mechanisms or on introducing a separate notion of second-class function. We introduce a novel approach based on modal effect types.
Paper Structure (72 sections, 28 theorems, 59 equations, 15 figures)

This paper contains 72 sections, 28 theorems, 59 equations, 15 figures.

Table of Contents

  1. Introduction
  2. Programming with Modal Effect Types
  3. From Function Arrows to Effect Contexts
  4. Overriding the Ambient Effect Context with Absolute Modalities
  5. Transforming the Ambient Effect Context with Relative Modalities
  6. Coercions Between Modalities
  7. Composing Handlers
  8. Storing Effectful Functions in Data Types
  9. Masking
  10. Kinds
  11. Polymorphism for Value Types
  12. Effect Polymorphsim
  13. A Tale of Locks and Keys: Elaborating Metl into Met
  14. A Multimodal Core Calculus with Effect Handlers
  15. Syntax
  16. ...and 57 more sections

Key Result

lemma 1

We have $\mu_F\Rightarrow\nu_F$ if and only if $\mu(F')\leqslant\nu(F')$ for all $F'$ with $F\leqslant F'$.

Figures (15)

  • Figure 1: Representative kinding, well-formedness, and auxiliary rules for Met.
  • Figure 2: Typing rules for Met.
  • Figure 3: Typing rules of $\mathrm{F}^1_{\mathrm{eff}}$.
  • Figure 4: Representative bidirectional typing and elaboration rules for Metl.
  • Figure 5: Syntax of Met with all extensions.
  • ...and 10 more figures

Theorems & Definitions (32)

  • lemma 1: Semantics of modality transformation
  • definition 1: Normal Forms
  • theorem 1: Progress
  • theorem 2: Subject Reduction
  • definition 2: Well-scoped
  • lemma 2: Type preservation of encoding
  • definition 3: Normal Forms
  • lemma 3: Modes and modalities form a category
  • lemma 4: Modality transformations are 2-cells
  • lemma 5: Monotone modalities
  • ...and 22 more