A Typed Continuation-Passing Translation for Lexical Effect Handlers
Fri 17 Jun 2022 03:30 - 03:50 at Kon-Tiki - Semantics
Effect handlers are a language features which enjoys popularity in academia and is also gaining traction in industry. Programs use abstract effect operations and handlers provide meaning to them in a delimited scope. Each effect operation is handled by the dynamically closest handler. Using an effect operation outside of a matching handler is meaningless and results in an error. A type-and-effect system prevents such errors from happening.
Lexical effect handlers are a recent variant of effect handlers with a number of attractive properties. Just as with traditional effect handlers, programs use effect operations and handlers give meaning to them. But unlike with traditional effect handlers, the connection between effect operations and their handler is lexical. Consequently, they typically have different type-and-effect systems.
The semantics of lexical effect handlers as well as their implementations use multi-prompt delimited control. They rely on the generation of fresh labels at runtime, which associate effect operations with their handlers. This use of labels and multi-prompt delimited control is theoretically and practically unsatisfactory.
Our main result is that typed lexical effect handlers do not need the full power of multi-prompt delimited control. We present the first CPS translation for lexical effect handlers to pure System F. It preserves well-typedness and simulates the traditional operational semantics. Importantly, it does so without requiring runtime labels. The CPS translation can be used to study the semantics of lexical effect handlers as well as as an implementation technique.
Thu 16 JunDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 16:50 | |||
15:30 20mTalk | A Typed Continuation-Passing Translation for Lexical Effect Handlers PLDI Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Marius Müller University of Tübingen, Klaus Ostermann University of Tuebingen DOI | ||
15:50 20mTalk | Deep and Shallow Types for Gradual Languages PLDI Ben Greenman Brown University DOI | ||
16:10 20mTalk | Kleene Algebra Modulo Theories: A Framework for Concrete KATsDistinguished Paper Award PLDI Michael Greenberg Stevens Institute of Technology, Ryan Beckett Microsoft Research, USA, Eric Campbell Cornell University DOI Pre-print | ||
16:30 20mTalk | Semantic Soundness for Language Interoperability PLDI Daniel Patterson Northeastern University, Noble Mushtak Northeastern University, Andrew Wagner Northeastern University, Amal Ahmed Northeastern University (USA) DOI |
Fri 17 JunDisplayed time zone: Pacific Time (US & Canada) change
03:30 - 04:50 | |||
03:30 20mTalk | A Typed Continuation-Passing Translation for Lexical Effect Handlers PLDI Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Marius Müller University of Tübingen, Klaus Ostermann University of Tuebingen DOI | ||
03:50 20mTalk | Deep and Shallow Types for Gradual Languages PLDI Ben Greenman Brown University DOI | ||
04:10 20mTalk | Kleene Algebra Modulo Theories: A Framework for Concrete KATsDistinguished Paper Award PLDI Michael Greenberg Stevens Institute of Technology, Ryan Beckett Microsoft Research, USA, Eric Campbell Cornell University DOI Pre-print | ||
04:30 20mTalk | Semantic Soundness for Language Interoperability PLDI Daniel Patterson Northeastern University, Noble Mushtak Northeastern University, Andrew Wagner Northeastern University, Amal Ahmed Northeastern University (USA) DOI |