Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 09:22 - 09:44 at Sala I - Type Abstraction and Effects Chair(s): Benjamin Delaware

Proposed originally by Plotkin and Pretnar, algebraic effects and their handlers are a leading-edge approach to computational effects: exceptions, mutable state, nondeterminism, and such. Appreciated for their elegance and expressiveness, they are now progressing into mainstream functional programming languages. In this paper, we introduce and examine programming language constructs that back adoption of programming with algebraic effects on a larger scale in a modular fashion by providing mechanisms for abstraction. We propose two such mechanisms: existential effects (which hide the details of a particular effect from the user) and local effects (which guarantee that no code coming from the outside can interfere with a given effect). The main technical difficulty arises from the dynamic nature of coupling an effectful operation with the right handler during execution, but, as we show in this paper, a carefully designed type system can ensure that this will not break the abstraction. Our main contribution is a novel calculus for algebraic effects and handlers, called $\lambda^{\textsf{HEL}}$, equipped with local and existential algebraic effects, in which the dynamic nature of handlers is kept in check by typed runtime coercions. As a proof of concept, we present an experimental programming language based on our calculus, which provides strong abstraction mechanisms via an ML-style module system.

Thu 17 Jan

Displayed time zone: Belfast change

09:00 - 10:06
Type Abstraction and EffectsResearch Papers at Sala I
Chair(s): Benjamin Delaware Purdue University
09:00
22m
Talk
Abstraction-Safe Effect Handlers via Tunneling
Research Papers
Yizhou Zhang Cornell University, Andrew Myers Cornell University
Link to publication DOI Media Attached
09:22
22m
Talk
Abstracting Algebraic Effects
Research Papers
Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław
Link to publication DOI Media Attached
09:44
22m
Talk
Fully Abstract Module Compilation
Research Papers
Karl Crary Carnegie Mellon University
Link to publication DOI Media Attached File Attached