一种轻量级的类型与效果系统，用于验证安全性：通过基于约束的子类型推断来跟踪永久性和临时性的失效情况

《Proceedings of the ACM on Programming Languages》：A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation with Constraint-Based Subtype Inference

本文提出一种高阶多态类型与效应系统，通过布尔代数类型精确建模副作用，实现资源永久与临时失效的静态追踪，并给出完整类型推断算法，应用于内存管理、迭代器失效、并发等领域。

　　

摘要

在许多编程范式中，某些程序实体仅在程序的特定范围内有效，例如那些可能在特定作用域结束时被自动释放的资源。一旦超出这些作用域，相应的实体就不再有效——它们会被永久性地标记为无效。有时，即使在资源的有效作用域内，对该资源的使用也可能暂时失效，例如在遍历可变集合时，因为遍历过程中修改集合可能会导致未定义行为。然而，高级通用编程语言很少允许在类型层面反映这些信息。以往解决这一问题的方法大多依赖于限制变量的别名或捕获行为，但这会降低语言的表达能力。在本文中，我们提出了一种更高层次的多态类型-效应系统，可以静态地跟踪敏感值和资源的永久性及临时性失效情况，而无需任何别名或捕获限制。我们使用布尔代数类型（并集、交集和否定运算）来精确建模程序项的副作用，并确保它们的使用是安全的（即不会导致失效）。此外，我们还提出了一种完整且实用的类型推断算法，程序员只需为高阶和多态递归函数的类型添加注释即可。我们的系统名为InvalML，适用于多种需要跟踪失效情况的应用场景，包括基于栈和基于区域的内存管理、迭代器失效处理、无数据竞争的并发编程、可变状态的封装、类型安全的异常处理和效应处理机制，甚至作用域安全的元编程。