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.

翻译：【摘要】我们提出了一种新颖的方法，将线性类型与效果处理器进行稳妥结合。线性类型系统能静态确保文件句柄等资源被精确使用一次；效果处理器则提供模块化编程抽象，支持从异常到并发等特性的实现。线性类型系统默认延续体恰好调用一次，而效果处理器允许延续被丢弃或多次调用——这种不匹配导致现有系统（如编程语言Links）中出现健全性问题，该语言将线性类型（用于会话类型）与效果处理器结合。我们提出控制流线性概念，确保延续体的使用能与其捕获资源的线性特性保持一致，从而消除此类健全性问题。我们在配备线性类型、效果类型和效果处理器的System F风格核心演算Feffpop中形式化定义了控制流线性。通过定义线性感知语义，我们正式证明Feffpop能维护线性值的完整性——即不会出现线性值被丢弃或复制的情况。为了展示控制流线性性的实用性，我们基于Feffpop的设计改进了Links语言，修复了长期存在的健全性缺陷。最后为充分发掘控制流线性潜力，我们基于限定类型定义了ML风格核心演算Qeffpop，它无需程序员提供标注，完全依赖类型推断推导控制流线性性——线性特性和效果均由限定类型捕获。Qeffpop克服了Feffpop的诸多实际限制，支持线性抽象、类型变量间的线性依赖关系，以及更细粒度的控制流线性概念。