Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. Abstraction-Safe Effect Handlers via Tunneling: Technical Report

Abstraction-Safe Effect Handlers via Tunneling: Technical Report

File(s)
tr.pdf (913.33 KB)
Permanent Link(s)
https://hdl.handle.net/1813/60202
Collections
Computing and Information Science Technical Reports
Author
Zhang, Yizhou
Abstract

Algebraic effect handlers offer a unified approach to expressing control-flow transfer idioms such as exceptions, iteration, and async/await. Unfortunately, previous attempts to make these handlers type-safe have failed to support the fundamental principle of modular reasoning for higher-order abstractions. We demonstrate that abstraction-safe algebraic effect handlers are possible by giving them a new semantics. The key insight is that code should only handle effects it is aware of. In our approach, the type system guarantees all effects are handled, but it is impossible for higher-order, effect-polymorphic code to accidentally handle effects raised by functions passed in; such effects tunnel through the higher-order, calling procedures polymorphic to them. By contrast, the possibility of accidental handling threatens previous designs for algebraic effect handlers. We prove that our design is not only type-safe, but also abstraction-safe. Using a logical-relations model that we prove sound with respect to contextual equivalence, we derive previously unattainable program equivalence results. Our mechanism offers a viable approach for future language designs aiming for effect handlers with strong abstraction guarantees.

Sponsorship
National Science Foundation (grant 1513797)
NASA (grant NNX16AB09G)
Date Issued
2018-11-09
Keywords
programming languages
•
type systems
•
effects
Related Version
This is a technical report accompanying "Abstraction-Safe Effect Handlers via Tunneling", appearing in POPL 2019.
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance