Reachability types are a recent proposal that has shown promise in scaling to higher-order but monomorphic settings, tracking aliasing and separation on top of a substrate inspired by separation logic. The prior $\lambda^*$ reachability type system qualifies types with sets of reachable variables and guarantees separation if two terms have disjoint qualifiers. However, naive extensions with type polymorphism and/or precise reachability polymorphism are unsound, making $\lambda^*$ unsuitable for adoption in real languages. Combining reachability and type polymorphism that is precise, sound, and parametric remains an open challenge. This paper presents a rethinking of the design of reachability tracking and proposes a solution to the key challenge of reachability polymorphism. Instead of always tracking the transitive closure of reachable variables as in the original design, we only track variables reachable in a single step and compute transitive closures only when necessary, thus preserving chains of reachability over known variables that can be refined using substitution. To enable this property, we introduce a new freshness qualifier, which indicates variables whose reachability sets may grow during evaluation steps. These ideas yield the simply-typed $\lambda^\diamond$-calculus with precise lightweight, i.e., quantifier-free, reachability polymorphism, and the $\mathsf{F}_{<:}^\diamond$-calculus with bounded parametric polymorphism over types and reachability qualifiers. We prove type soundness and a preservation of separation property in Coq.

翻译：可达类型是近期提出的方法，在扩展到高阶但单态的场景中展现出潜力——它在受分离逻辑启发的基底上追踪别名与分离。先前的$\lambda^*$可达类型系统用可达变量集限定类型，并保证如果两个项具有不相交的限定符则它们是分离的。然而，朴素扩展的类型多态和/或精确可达多态会导致不一致，使得$\lambda^*$不适合应用于实际语言。同时实现精确、一致且参数化的可达性与类型多态仍是一个开放挑战。本文重新思考了可达追踪的设计，并提出了可达多态这一关键问题的解决方案。与原始设计中始终追踪可达变量的传递闭包不同，我们仅追踪单步可达的变量，仅在必要时计算传递闭包，从而保留已知变量上的可达链（这些链可通过替换进行精化）。为实现此特性，我们引入了新的新鲜性限定符，该限定符标识其可达集可能在求值步骤中增长的变量。这些思想产生了具有精确轻量级（即无量词）可达多态的简单类型$\lambda^\diamond$-演算，以及具有类型和可达限定符上有界参数多态的$\mathsf{F}_{<:}^\diamond$-演算。我们在Coq中证明了类型安全性以及分离保持性质。