Projects per year
Abstract / Description of output
We propose a novel approach to soundly combining linear types with multi-shot effect handlers. circear type systems statically ensure that resources such as file handles and communication channels are used exactly once. Effect handlers provide a rich modular programming abstraction for implementing features ranging from exceptions to concurrency to backtracking. Whereas conventional linear type systems bake in the assumption that continuations are invoked exactly once, effect handlers allow continuations to be discarded (e.g. for exceptions) or invoked more than once (e.g. for backtracking). 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 the notion of control-flow linearity in a System F-style core calculus Feff∘ equipped with linear types, an effect type system, and effect handlers. We define a linearity-aware semantics in order to formally prove that Feff∘ 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 circks based on the design of Feff∘, 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 Qeff∘, 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. Qeff∘ overcomes a number of practical limitations of Feff∘, supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control-flow linearity.
We formalise the notion of control-flow linearity in a System F-style core calculus Feff∘ equipped with linear types, an effect type system, and effect handlers. We define a linearity-aware semantics in order to formally prove that Feff∘ 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 circks based on the design of Feff∘, 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 Qeff∘, 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. Qeff∘ overcomes a number of practical limitations of Feff∘, supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control-flow linearity.
Original language | English |
---|---|
Article number | 54 |
Pages (from-to) | 1600–1628 |
Number of pages | 29 |
Journal | Proceedings of the ACM on Programming Languages |
Volume | 8 |
Issue number | POPL |
DOIs | |
Publication status | Published - 5 Jan 2024 |
Event | 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024) - London, United Kingdom Duration: 17 Jan 2024 → 19 Jan 2024 Conference number: 51 https://popl24.sigplan.org/ |
Fingerprint
Dive into the research topics of 'Soundly Handling Linearity'. Together they form a unique fingerprint.Projects
- 1 Finished