An Effect System for Algebraic Effects and Handlers

TL;DR

This paper introduces an effect system for core Eff, a simplified language with algebraic effects and handlers, providing safety proofs, a denotational semantics, and tools for reasoning about program equivalences.

Contribution

It develops an expressive effect system for core Eff, proves its safety and adequacy, and provides reasoning tools for contextual equivalences, including equations for mutable state.

Findings

Proves safety of the operational semantics.

Provides a denotational semantics using Pitts's theory.

Derives equations for mutable state and non-interfering references.

Abstract

We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with respect to it. Then we give a domain-theoretic denotational semantics of core Eff, using Pitts's theory of minimal invariant relations, and prove it adequate. We use this fact to develop tools for finding useful contextual equivalences, including an induction principle. To demonstrate their usefulness, we use these tools to derive the usual equations for mutable state, including a general commutativity law for computations using non-interfering references. We have formalized the effect system, the operational semantics, and the safety theorem in Twelf.