Preprint
Soundly Handling Linearity
ArXiv.org
07/18/2023
DOI: 10.48550/arxiv.2307.09383
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 Feffpop
equipped with linear types, effect types, and effect handlers. We define a
linearity-aware semantics to formally prove that Feffpop preserves the
integrity of linear values in the sense that no linear value is discarded or
duplicated. In order to show that control flow linearity can be made practical,
we adapt Links based on the design of Feffpop, in doing so fixing a
long-standing soundness bug.
Finally, to better expose the potential of control flow linearity, we define
an ML-style core calculus Qeffpop, based on qualified types, which requires no
programmer provided annotations, and instead relies entirely on type inference
to infer control flow linearity. Both linearity and effects are captured by
qualified types. Qeffpop overcomes a number of practical limitations of
Feffpop, supporting abstraction over linearity, linearity dependencies between
type variables, and a much more fine-grained notion of control flow linearity.
Details
- Title: Subtitle
- Soundly Handling Linearity
- Creators
- Wenhao TangDaniel HillerströmSam LindleyJ. Garrett Morris
- Resource Type
- Preprint
- Publication Details
- ArXiv.org
- DOI
- 10.48550/arxiv.2307.09383
- ISSN
- 2331-8422
- Language
- English
- Date posted
- 07/18/2023
- Academic Unit
- Computer Science
- Record Identifier
- 9984445623502771
Metrics
12 Record Views