一句话:提出带生命周期借用的纯函数语言及全自动类型推断,并可按需插入引用计数以保证可类型化。
论文旨在让用户无需标注即可享受带生命周期借用带来的性能收益。作者设计了一种带借用的纯函数语言与类型系统,并给出全自动类型推断:当程序无法通过类型检查时,推断过程会插入少量引用计数操作使其可被类型化。文章为借用语言给出堆语义,并证明良类型程序不会破坏内存安全。作者将该内存管理策略实现于 Morphic 语言栈,并与基于线性类型推断的 Perceus 比较。结果显示,在所有基准上几乎消除了全部引用计数操作,引用计数增量降低 75%–100%,总体取得 1.48 倍几何平均加速。
We present a new pure functional language and type system with borrows with lifetimes, and a corresponding fully-automatic type inference procedure. Inference provides users the performance benefits of borrows with lifetimes without requiring user annotation. If the user’s program cannot be typed, inference inserts a handful of reference count operations so that it can be typed. We provide a heap semantics for our borrowing language and prove a soundness theorem, guaranteeing that well-typed programs do not violate memory safety. We implement our memory management strategy as part of the Morphic language stack and compare it to Perceus, a state-of-the-art reference-counting technique based on linear type inference. We find that our system is able to eliminate almost all reference count operations across a range of programs, reducing reference count increments by 75–100% on all benchmarks with reference count increments under the baseline. As a result, we achieve a 1 . 48× geomean speedup overall on all benchmarks.
@article{paperbot3779,
title = {Fully-Automatic Type Inference for Borrows with Lifetimes},
author = {William Brandon and Benjamin Driscoll and Frank Dai and Jonathan Ragan-Kelley and Mae Milano and Alex Aiken},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798221}
}