Contextual Modal Types for Algebraic Effects and Handlers

TL;DR

This paper introduces ECMTT, a novel calculus that models algebraic effects using contextual modal types, providing a type system that inherently tracks effects through logical constructs, bridging effects and modal logic.

Contribution

ECMTT is the first system to connect algebraic effects with modal types, offering a logical foundation for effect tracking within a type system.

Findings

ECMTT achieves local soundness and completeness.

Operational semantics are defined by β-reduction.

Effect handlers naturally emerge as context transitions.

Abstract

Programming languages with algebraic effects often track the computations' effects using type-and-effect systems. In this paper, we propose to view an algebraic effect theory of a computation as a variable context; consequently, we propose to track algebraic effects of a computation with \emph{contextual modal types}. We develop ECMTT, a novel calculus which tracks algebraic effects by a contextualized variant of the modal $\Box$ (necessity) operator, that it inherits from Contextual Modal Type Theory (CMTT). Whereas type-and-effect systems add effect annotations on top of a prior programming language, the effect annotations in ECMTT are inherent to the language, as they are managed by programming constructs corresponding to the logical introduction and elimination forms for the $\Box$ modality. Thus, the type-and-effect system of ECMTT is actually just a type system. Our design obtains the properties of local soundness and completeness, and determines the operational semantics solely by $\beta$-reduction, as customary in other logic-based calculi. In this view, effect handlers arise naturally as a witness that one context (i.e., algebraic theory) can be reached from another, generalizing explicit substitutions from CMTT. To the best of our knowledge, ECMTT is the first system to relate algebraic effects to modal types. We also see it as a step towards providing a correspondence in the style of Curry and Howard that may transfer a number of results from the fields of modal logic and modal type theory to that of algebraic effects.