Avoid Arguments and Escape with Your Self: Expressive Subtyping and Decidable Bidirectional Checking for Reachability Types
<|reference_start|>Avoid Arguments and Escape with Your Self: Expressive Subtyping and Decidable Bidirectional Checking for Reachability Types: Despite Rust's success in systems programming, its ``shared XOR mutable'' principle significantly restricts how mutable values can be used, precluding many useful functional programming idioms. Reachability types are a recent proposal to address the key limitations of Rust-style approaches by tracking, rather than prohibiting, shared, escaping, and mutable data, even in the presence of higher-order functions and polymorphic types. The key to enabling such expressiveness is the notion of self-references in reachability qualifiers. However, self-references present major challenges in designing expressive subtyping and decidable type checking algorithms, since self-references are neither fully covariant nor fully contravariant, yet still need to vary in certain circumstances. This lack of an effective type checking algorithm is a key impediment toward making reachability types truly practical, and leveraging them to bring the benefits of programming with lifetimes and sharing to practical higher-level languages.   In this paper, we investigate the issues of subtyping and type checking of self-references for reachability types. We address key gaps in previous work by proposing a refined notion of subtyping, which more smoothly supports features such as Church-encoded datatypes, making the overall system more expressive. We also develop a sound and decidable bidirectional type checking algorithm, implemented and verified in Coq.<|reference_end|>
@article{jia2024avoid,
    title={Avoid Arguments and Escape with Your Self: Expressive Subtyping and
  Decidable Bidirectional Checking for Reachability Types},
    author={Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf},
    journal={arXiv preprint arXiv:2404.08217},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.08217},
    primaryClass={cs.PL}
}