Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminars LFCS seminar: Tom Schrijvers: Explicit effect subtyping

LFCS seminar: Tom Schrijvers: Explicit effect subtyping

— filed under: ,

  • LFCS Seminar
  • Upcoming events
When Jan 23, 2018
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal


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.

This is joint work with Amr Hany Saleh, Georgios Karachalias and Matija Pretnar.



Document Actions