Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types

TL;DR

This paper introduces a novel sound and decidable bidirectional type checking algorithm for reachability types that effectively handles avoidance through subtyping, enabling the verification of complex escaping data types.

Contribution

It presents the first algorithmic approach for reachability types with formal soundness, using subtyping-based avoidance and mechanized in Lean.

Findings

Proposes a refined declarative reachability type system with self-aware subtyping.

Develops a bidirectional type system that infers qualifiers via unification.

Successfully type-checks complex escaping Church-encoded data types.

Abstract

Algorithmic type checking and inference of reachability types present a particular challenge with regards to subtyping. As a restricted form of dependent types, reachability types are subject to the avoidance problem: a variable mentioned in types becomes ill-scoped when its defining scope ends. Prior works thus introduce self-references, akin to this pointers in OO languages, to replace the escaping variable, so that an escaping object's this pointer can serve as the new logical owner of any captured resources. Nevertheless, conversions involving self-references require reasoning about function qualifiers. As prior work isolates subtyping judgements from associated qualifiers, their system requires manually-inserted term-level coercions (i.e., $\eta$-expansion) to support escaping values. This, of course, is highly unsatisfactory for algorithmic avoidance. In this work, we propose the first typing algorithm for reachability types with formal soundness guarantees, and with an avoidance strategy based entirely on subtyping. We first present a refined declarative reachability type system, $G_{<:}^\blacklozenge$, which includes an expressive self-aware subtyping theory for self-references, and is built on algorithmic contexts where holes can reside in partially specified qualifiers. On top of that, we develop the bidirectional typing system, $G_\leftrightharpoons^\blacklozenge$, which infers qualifiers by a lightweight unification mechanism, and converts types automatically for avoidance. $G_{<:}^\blacklozenge$ is proven sound by a logical relation, and $G_\leftrightharpoons^\blacklozenge$ is proven decidable and sound with respect to $G_{<:}^\blacklozenge$. The result is an end-to-end formally verified type checker, implemented and mechanized in Lean, which is able to type-check challenging example programs such as escaping Church-encoded data types.