一句话：提出控制流线性，使线性类型与多次调用效应处理器可靠结合，形式化验证并修复 Links 缺陷。
线性类型系统通常假设续延恰好调用一次，而效应处理器允许丢弃（异常）或多次调用（回溯）续延，二者结合会破坏可靠性，Links 便会话类型与效应处理器结合存在长期缺陷。本文提出控制流线性，确保续延使用符合其捕获资源的线性约束。作者在带线性类型、效应类型与效应处理器的 System F 风格核心演算 F_eff^∘ 中形式化，给出线性敏感语义并证明线性值不会被丢弃或复制，据此修复 Links 缺陷。进一步提出基于限定类型的 ML 风格演算 Q_eff^∘，无需程序员标注，完全由类型推断推断控制流线性，支持线性抽象、类型变量间线性依赖和更细粒度控制流线性。
We propose a novel approach to soundly combining linear types with multi-shot effect handlers. Linear 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 F eff ∘ equipped with linear types, an effect type system, and effect handlers. We define a linearity-aware semantics in order to formally prove that F eff ∘ 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 F eff ∘ , 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 Q eff ∘ , 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. Q eff ∘ overcomes a number of practical limitations of F eff ∘ , supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control-flow linearity.
@article{paperbot2631,
title = {Soundly Handling Linearity},
author = {Wenhao Tang and Daniel Hillerström and Sam Lindley and J. Garrett Morris},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632896}
}