paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Fully-Automatic Type Inference for Borrows with Lifetimes

面向带生命周期借用的全自动类型推断
OOPSLA 10(OOPSLA1)2026匹配度 3/10 · 论文属于类型系统与静态分析/内存管理方向,具有形式化语义与工程实现,但与用户核心关注的 PL 与 AI/LLM/Agent 交叉、浮点程序分析、贝叶斯程序分析均无直接关联,仅方法层面有一定借鉴意义。引用 0 inbox
William Brandon, Benjamin Driscoll, Frank Dai, Jonathan Ragan-Kelley, Mae Milano, Alex Aiken
crossref: 2026-09-10

AI 速览

一句话:提出带生命周期借用的纯函数语言及全自动类型推断,并可按需插入引用计数以保证可类型化。

论文旨在让用户无需标注即可享受带生命周期借用带来的性能收益。作者设计了一种带借用的纯函数语言与类型系统,并给出全自动类型推断:当程序无法通过类型检查时,推断过程会插入少量引用计数操作使其可被类型化。文章为借用语言给出堆语义,并证明良类型程序不会破坏内存安全。作者将该内存管理策略实现于 Morphic 语言栈,并与基于线性类型推断的 Perceus 比较。结果显示,在所有基准上几乎消除了全部引用计数操作,引用计数增量降低 75%–100%,总体取得 1.48 倍几何平均加速。

问题
如何在不要求用户编写生命周期标注的情况下,获得借用与生命周期带来的性能收益,同时保证内存安全。
方法
设计带借用的纯函数语言与类型系统,提出全自动类型推断,并在无法类型化时插入少量引用计数操作,且给出堆语义与可靠性证明。
评估
在 Morphic 语言栈中实现,与 Perceus 对比;多数程序几乎消除引用计数操作,增量降低 75–100%,整体几何平均加速 1.48 倍。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}