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的一些实际限制，支持对线性性的抽象、类型变量之间的线性依赖关系，以及更细粒度的控制流线性概念。