Contextual Modal Types for Algebraic Effects and Handlers

Programming languages with algebraic effects often rely on effect annotations to track algebraic operations in a computation. This is particularly important in the presence of effect handlers, where handling of an effect may remove it from the annotation in the computation's type. In this paper we view the algebraic effect theory of a computation as a variable context, and track the effects directly in computation's modal type with ECMTT, a novel calculus for algebraic effects and handlers. Our calculus supports computations with effects and derives from Contextual Modal Type Theory (CMTT), from which it inherits a number of important logical properties. In contrast to type-and-effect systems, where effects are attached as annotations to a prior computational language, ECMMT tracks effects by a contextualized variant of the modal $\Box$ (necessity) operator of the intuitionistic modal logic of CMTT. In programming, the effect annotations are explicitly managed by the dedicated term constructors corresponding to the logical introduction and elimination forms for the modality. The modal foundation leads to customary logical properties of local soundness and completeness, and determines the operational semantics of ECMTT directly by $\beta$-reduction. In addition, effect handlers become a generalization of explicit substitutions, which in CMTT serve to reach one context from another. 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.