妥善处理线性
摘要：线性类型和效果处理器的声音组合的新方法的提出。线性类型系统静态地确保资源（如文件句柄）仅被使用一次。效果处理器提供了一种模块化编程抽象，用于实现从异常到并发等各种功能。而线性类型系统则固定了继续被调用一次的假设，效果处理器允许继续被丢弃或多次调用。这种不匹配导致现有系统（如编程语言Links）中存在声音错误。我们引入了控制流线性作为一种手段，以确保继续根据其捕捉的任何资源的线性使用，从而排除这种声音错误。 我们在一种带有线性类型、效果类型和效果处理器的System F风格核心计算机Feffpop中形式化控制流线性。我们定义了一个线性感知的语义，以正式证明Feffpop在维护线性值的完整性方面，没有丢弃或复制任何线性值。为了展示控制流线性可以变得实用，我们根据Feffpop的设计改进了Links，从而修复了一个长期存在的声音错误。 最后，为了更好地展示控制流线性的潜力，我们定义了一个基于限定类型的ML风格核心计算器Qeffpop，它不需要程序员提供的注释，而是完全依赖于类型推导来推断控制流线性。线性和效果都由限定类型捕捉。Qeffpop克服了Feffpop的一些实际限制，支持线性抽象、类型变量之间的线性依赖以及更细粒度的控制流线性概念。
作者：Wenhao Tang, Daniel Hillerstr"om, Sam Lindley, J. Garrett Morris
论文ID：2307.09383
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-19