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's result 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.

翻译：在存在变量修改和别名的情况下对程序进行推理是众所周知的难题。Rust在系统编程中推广了基于生命周期的所有权追踪，但其"共享异或可变"模型从根本上与高阶函数式编程相悖。可达类型提供了一种替代方案：通过追踪每个表达式结果可到达的资源，实现可变数据的安全共享与逃逸。为追踪复杂对象图内部的到达关系，可达类型采用自引用机制，允许组件像面向对象语言中的`this`指针一样从内部引用外围资源。虽然自引用对逃逸数据的声明式类型化很自然，但它使子类型关系及类型推断变得复杂：变体限制了自引用的出现位置，而有用的类型转换必须允许自引用在可控范围内变化，这反过来对推断施加了约束。不理想的结果是，先前的工作要求程序员即使在回避（避免类型中作用域不合法的名称）时也要插入术语级强制转换。鉴于先前工作均为声明式，本文研究算法化可达类型。我们引入一种更精细的子类型关系，允许更灵活地使用自引用。我们进一步开发了可靠且可判定的双向类型算法，并在Lean中实现验证。该算法能自动避免类型中作用域不合法的名称，并通过轻量级合一机制推断限定符。作为迈向实用可达编程的一步，我们证明该系统能在无需显式强制转换的情况下，追踪复杂邱奇编码数据类型中的多样化可达模式。