Local Algebraic Effect Theories

TL;DR

This paper introduces a novel type system for algebraic effects that tracks equations within subprograms, enhancing reasoning, safety, and enabling practical optimizations.

Contribution

It proposes a new approach where the type system observes equations in subparts, improving flexibility and soundness over traditional trivial theories.

Findings

Provides a sound and flexible logic for algebraic effects

Enables practical optimizations based on tracked equations

Improves reasoning and safety in effect handling

Abstract

Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety. We present an alternative approach where the type system tracks equations that are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimizations and reasoning tools.