Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs

Fueled by the success of Rust, many programming languages are adding substructural features to their type systems. The promise of tracking properties such as lifetimes and sharing is tremendous, not just for low-level memory management, but also for controlling higher-level resources and capabilities. But so are the difficulties in adapting successful techniques from Rust to higher-level languages, where they need to interact with other advanced features, especially various flavors of functional and type-level abstraction. Hence, recent proposals such as Scala's Capture Types target far narrower domains than Rust. But what would it take to bring full-fidelity reasoning about lifetimes and sharing to mainstream languages? 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 𝜆 * 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 𝜆 * 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 𝜆 -calculus with precise lightweight, i.e., quantifier-free, reachability polymorphism, and the F <: -calculus with bounded parametric polymorphism over types and reachability qualifiers. We prove type soundness and a preservation of separation property in Coq. We show that our system subsumes both previous reachability type systems as well as the essence of Scala's capture types, making true tracking of lifetimes and sharing practical for mainstream languages.