线性效应、异常与资源安全：析构函数的 Curry-Howard 对应

我们分析了在抽象编程语言模型中组合线性、效应和异常问题，即为单子 $T(- \oplus E)$ 提供某种强度在线性环境中的问题。我们特别考虑 $T$ 为分配单子，这是我们引入的用于建模和研究资源安全性的单子。我们将这些结果应用于一系列两个线性效应计算器，我们为它们建立了资源安全性属性。第一个计算器是一个线性（可选有序）调用-by-push-value 语言，包含两种分配效应 $\mathbf{new}$ 和 $\mathbf{delete}$。资源安全性属性源于类型的线性和有序特性。随后，我们通过在类型中添加默认析构操作来将异常与线性和效应集成，灵感来自 C++/Rust 的析构函数。在本文中，我们将析构函数视为切片类别中对象 $\delta : A\rightarrow TI$。这种构造导致第二个计算器，资源调用-by-push-value，具有异常和析构函数，其弱化和交换规则执行副作用。因此，它在类型层面上是仿射的，但在导演层面上是有序的。正如在 C++ 和 Rust 中，一个“移动”操作——即副作用的交换规则——对于以随机顺序释放资源（而非后进先出顺序）是必需的。