当生命期获得解放：一种带有高阶可达性追踪的 Arena 类型系统
编程语言
2026-03-31 v3
摘要
由于控制、表达能力和灵活性之间的张力，语言中的静态资源管理仍然具有挑战性。基于区域的系统 [Grossman et al. 2002; Tofte et al. 2001] 通过词法作用域区域提供批量释放，其中所有分配遵循栈规则。然而，区域及其资源都是二等公民，既不能逃逸出其作用域，也不能被自由返回。以 Rust [Clarke et al. 2013] 为代表的所有权与线性类型系统提供了非词法生命期和稳健的静态保证，但依赖于限制高阶模式和表达性共享的不变量。在本工作中，我们提出了一种统一这些优势的新型类型系统。我们的系统将所有堆分配资源视为一等值，同时允许程序员通过三种分配模式控制生命期与粒度：(1) 用于单独、非词法引用的新鲜分配；(2) 随后将在影子 arena 内集体分组资源的协同分配；(3) 遵循栈规则且具有词法有界生命期的作用域分配。无论采用何种模式，所有资源共享统一类型，在泛型抽象中没有区别，从而保持了语言的高阶参数化特性。在具有灵活共享的高阶语言中实现静态安全性并非易事。我们通过扩展可达性类型 [Wei et al. 2024] 来集体追踪一等资源，并采用流不敏感的释放推理来实现选择性栈规则，从而解决了这一问题。这些机制在 Rocq 中产生了 Aq<: 和 {A}q<:，两者均被形式化并证明具有类型安全性和内存安全性。
引用
@article{arxiv.2509.04253,
title = {When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking},
author = {Siyuan He and Songlin Jia and Yuyan Bao and Tiark Rompf},
journal= {arXiv preprint arXiv:2509.04253},
year = {2026}
}