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.
In this talk, I will present polymorphic reachability types, a recent proposal has shown promise in scaling lifetime reasoning to higher-order and polymorphic settings, tracking aliasing and separation on top of a substrate inspired by separation logic. More specifically, I will present the simply-typed λ◆-calculus with precise lightweight (quantifier-free) reachability polymorphism, and the F◆<:-calculus with bounded parametric polymorphism over types and reachability qualifiers. I will also discuss meta-theory results, safe capability programming patterns enabled by reachability types, and flow-sensitive effect system extensions.
