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

TL;DR

This paper introduces a new approach to reachability types that supports precise, sound, and parametric polymorphism in higher-order programs, improving upon prior systems by tracking variable reachability more efficiently.

Contribution

It proposes a novel design for reachability polymorphism that tracks only immediate reachability, introduces a freshness qualifier, and formalizes the system with proofs in Coq.

Findings

Proposes a new reachability tracking method that is more precise and efficient.

Develops a type system with lightweight, quantifier-free reachability polymorphism.

Proves type soundness and separation preservation in Coq.

Abstract

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.