Modal Effect Types

TL;DR

This paper introduces modal effect types as a novel approach to effect handling, enabling static effect management without extensive annotations or fragile mechanisms, thereby improving robustness and usability.

Contribution

It proposes modal effect types to handle effects statically without requiring extensive annotations or fragile syntactic mechanisms, advancing effect system design.

Findings

Modal effect types enable static effect handling.

The approach reduces the need for extensive effect annotations.

It offers a more robust alternative to existing effect systems.

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.