一句话：提出首个可靠且可判定的可达性类型双向类型检查算法，自动规避类型中不合作用域的名字，并在 Lean 中机器验证。
在存在变异与别名时进行程序推理十分困难。可达性类型（reachability types）通过追踪表达式可触及的资源，支持可变数据的安全共享与逃逸，并借助 self 引用刻画复杂对象图内部的可达性，类似面向对象语言中的 this 指针。然而 self 引用使子类型与类型推断变得复杂：变型（variance）限制了 self 引用的出现位置，而有用的类型转换又必须允许其受控变化，从而约束推断；已有工作均为声明式，且即便仅做 avoidance（避免类型中出现不合作用域的名字）也要求程序员插入项层 coercion。本文研究算法化的可达性类型，提出更精化的子类型关系以更灵活地使用 self 引用，并给出一个可靠且可判定的双向类型检查算法，在 Lean 中实现并验证。该算法自动避免类型中的不合作用域名字，并通过轻量合一机制推断 qualifier。实验表明，系统能在复杂的 Church 编码数据类型上追踪多种可达性模式，而无需显式 coercion。
Reasoning about programs in the presence of mutation and aliasing is notoriously difficult. Rust has popularized lifetime-based ownership tracking in systems programming, but its “shared XOR mutable” model is fundamentally at odds with higher-level functional programming. Reachability types offer an alternative: they enable safe sharing and escape of mutable data by tracking which resources each expression can reach. To track internal reachability within complex object graphs, reachability types adopt self-references that let components refer to enclosing resources from inside, just like this pointers in OO languages. While natural for declaratively typing escaping data, self-references complicate subtyping and furthermore type inference: variance restricts where self-references may appear, yet useful type conversions must allow them to vary in controlled ways, which in turn imposes constraints on inference. As an undesirable result, prior works require programmers to insert term-level coercions for even just avoidance —avoiding ill-scoped names in types. With all prior works being declarative, we investigate algorithmic reachability types in this work. We introduce a refined subtyping relation that permits more flexible usages of self-references. We further develop a sound and decidable bidirectional typing algorithm, implemented and verified in Lean. The algorithm automatically avoids ill-scoped names in types, and infers qualifiers via a lightweight unification mechanism. As a step towards practical reachability programming, we show that the system is capable of tracking diverse reachability patterns without explicit coercions in complex Church-encoded datatypes.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{JiaWHBR26,
title = {Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types},
author = {Songlin Jia and Guannan Wei and Siyuan He and Yuyan Bao and Tiark Rompf},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808335}
}