Soundly Handling Linearity
Wenhao Tang, Daniel Hillerstr\"om, Sam Lindley, J. Garrett Morris

TL;DR
This paper introduces control flow linearity, a new approach to ensure sound handling of linear resources with effect handlers, formalized in a core calculus and applied to fix bugs in existing languages like Links.
Contribution
It formalizes control flow linearity in a core calculus, proving its soundness, and adapts it to practical languages, fixing longstanding bugs and enhancing type inference capabilities.
Findings
Feffpop preserves linear resource integrity.
Applying control flow linearity fixes soundness bugs in Links.
Qeffpop enables type inference for control flow linearity without annotations.
Abstract
We propose a novel approach to soundly combining linear types with effect handlers. Linear type systems statically ensure that resources such as file handles are used exactly once. Effect handlers provide a modular programming abstraction for implementing features ranging from exceptions to concurrency. Whereas linear type systems bake in the assumption that continuations are invoked exactly once, effect handlers allow continuations to be discarded or invoked more than once. This mismatch leads to soundness bugs in existing systems such as the programming language Links, which combines linearity (for session types) with effect handlers. We introduce control flow linearity as a means to ensure that continuations are used in accordance with the linearity of any resources they capture, ruling out such soundness bugs. We formalise control flow linearity in a System F-style core calculus…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
