Explicit Effect Subty**
Authors:
Georgios Karachalias,
Matija Pretnar,
Amr Hany Saleh,
Stien Vanderhallen,
Tom Schrijvers
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 subty**-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,…
▽ More
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 subty**-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 subty**-based type-and-effect system. It reifies appeals to subty** in explicit casts with coercions that witness the subty** proof, quickly exposing ty** bugs in program transformations.
Our ty**-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.
△ Less
Submitted 28 May, 2020;
originally announced May 2020.
