Soundly Handling Linearity
Soundly Handling Linearity
复制标题
妥善处理线性
DOI：
10.1145/3632896
复制
发表时间：
2024
影响因子：
--
通讯作者：
Morris, J. Garrett
中科院分区：
文献类型：
--
作者：
Tang, Wenhao;Hillerström, Daniel;Lindley, Sam;Morris, J. Garrett
我们提出了一种新的方法来合理地结合线性类型与多镜头效果处理程序。Circear型系统静态地确保诸如文件句柄和通信信道之类的资源只被使用一次。效果处理程序提供了丰富的模块化编程抽象，用于实现从异常到并发再到回溯的各种特性。传统的线性类型系统假设延续只被调用一次，而效果处理程序允许延续被丢弃（例如异常）或调用多次（例如回溯）。这种不匹配导致现有系统中的可靠性错误，例如编程语言Links，它将线性（用于会话类型）与效果处理程序相结合。我们引入控制流线性作为一种手段，以确保继续使用根据线性的任何资源，他们捕获，排除这样的健全bugs.We正式的概念控制流线性的系统F风格的核心calculusFeff装备线性类型，效果类型系统，效果处理程序。我们定义了一个线性感知的语义，以正式证明thatFeff保留线性值的完整性，在这个意义上，没有线性值被丢弃或重复。为了证明控制流线性可以实现，我们在Feff函数的设计基础上修改了circks，这样做修复了一个长期存在的合理性bug。最后，为了更好地揭示控制流线性的潜力，我们定义了一个ML风格的核心演算Qeff函数，基于合格的类型，它不需要程序员提供注释，而是完全依赖于类型推断来推断控制流线性。线性和效果都由限定类型捕获。Qeff克服了Feff的许多实际限制，支持线性抽象、类型变量之间的线性依赖关系以及更细粒度的控制流线性概念。
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 calculusFeff∘equipped with linear types, an effect type system, and effect handlers. We define a linearity-aware semantics in order to formally prove thatFeff∘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 ofFeff∘, 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 calculusQeff∘, 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 ofFeff∘, supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control-flow linearity.