Explicit Effect Subtyping

TL;DR

This paper introduces an explicitly-typed core calculus for algebraic effect handlers with subtyping, improving error detection and enabling effective optimizations in effect-aware compilers.

Contribution

It presents a new explicitly-typed polymorphic calculus with subtyping and coercions, along with an inference algorithm and a translation to pure languages, enhancing reliability and optimization.

Findings

Coercions expose typing bugs in program transformations.

The calculus supports a straightforward erasure of effect information.

A monadic translation efficiently maps effects to pure language constructs.

Abstract

As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subtyping-based effect system on which an effect-aware optimizing compiler could be built. Unfortunately, in our experience, implementing optimizations for Eff is overly error-prone because its core language is implicitly-typed, making code transformations very fragile. To remedy this, we present an explicitly-typed polymorphic core calculus for algebraic effect handlers with a subtyping-based type-and-effect system. It reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof, quickly exposing typing bugs in program transformations. Our typing-directed elaboration comes with a constraint-based inference algorithm that turns an implicitly-typed Eff-like language into our calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content. Additionally, we present a monadic translation from our calculus into a pure language without algebraic effects or handlers, using the effect information to introduce monadic constructs only where necessary.