Matija Pretnar: Explicit Effect Subtyping

Datum objave: 8. 1. 2018
Seminar za temelje matematike in teoretično računalništvo
Torek, 9. 1. 2018, od 12h do 14h, Plemljev seminar, Jadranska 19

Joint work with Amr Hany Saleh, Georgios Karachalias, and 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 subtyping-based effect system on which an effect-aware optimising compiler could be built. Unfortunately, in our experience, implementing optimisations 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.