一句话：提出类型与效应系统 InvalML，用布尔代数类型追踪永久与临时失效，无需别名或捕获限制，并提供完备推断算法。
在许多编程范式中，程序实体仅在特定区域内有效：超出作用域后即被永久失效；而某些资源即使在有效范围内也可能被临时失效，例如在可变集合迭代期间修改集合会导致未定义行为。然而，通用高级语言很少在类型层面反映这类信息，已有方案多通过限制别名或变量捕获来实现，损害了语言表达力。本文提出一种高阶多态类型与效应系统，在不限制别名与捕获的前提下静态追踪敏感值与资源的永久和临时失效。系统采用布尔代数类型（并、交、补）精确建模程序项的副作用，并保证失效安全。作者还给出完备且实用的类型推断算法，程序员只需标注高阶及多态递归函数的类型。系统原型名为 InvalML，可应用于栈式与区域内存管理、迭代器失效、无数据竞争并发、可变状态封装、类型安全异常与效应处理器以及作用域安全元编程等场景。
In many programming paradigms, some program entities are only valid within delimited regions of the program, such as resources that might be automatically deallocated at the end of specific scopes. Outside their live scopes, the corresponding entities are no longer valid – they are permanently invalidated . Sometimes, even within the live scope of a resource, the use of that resource must become temporarily invalid , such as when iterating over a mutable collection, as mutating the collection during iteration might lead to undefined behavior. However, high-level general-purpose programming languages rarely allow this information to be reflected on the type level. Most previously proposed solutions to this problem have relied on restricting either the aliasing or the capture of variables, which can reduce the expressiveness of the language. In this paper, we propose a higher-rank polymorphic type-and-effect system to statically track the permanent and temporary invalidation of sensitive values and resources, without any aliasing or capture restrictions. We use Boolean-algebraic types (unions, intersections, and negations) to precisely model the side effects of program terms and guarantee they are invalidation-safe. Moreover, we present a complete and practical type inference algorithm, whereby programmers only need to annotate the types of higher-rank and polymorphically-recursive functions. Our system, nicknamed InvalML, has a wide range of applications where tracking invalidation is needed, including stack-based and region-based memory management, iterator invalidation, data-race-free concurrency, mutable state encapsulation, type-safe exception and effect handlers, and even scope-safe metaprogramming.
@article{paperbot2887,
title = {A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation with Constraint-Based Subtype Inference},
author = {Cunyuan Gao and Lionel Parreaux},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763144}
}