2023/11/13 by Edward Lee, Yaoyu Zhao, James You +4 · 1 voice
Computer Science · #Distributed systems and fault tolerance #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.PL
paper · pdf · doi:10.1145/3649832
arxiv published 2023/11/13 · arxiv updated 2023/11/13 · openalex publication_date 2024/04/29 · openalex created_date 2024/04/30 · openalex updated_date 2026/07/28
Type qualifiers offer a lightweight mechanism for enriching existing type systems to enforce additional, desirable, program invariants. They do so by offering a restricted but effective form of subtyping. While the theory of type qualifiers is well understood and present in many programming languages today, polymorphism over type qualifiers remains an area less well examined. We explore how such a polymorphic system could arise by constructing a calculus, System F-sub-Q, which combines the higher-rank bounded polymorphism of System F-sub with the theory of type qualifiers. We explore how the ideas used to construct System F-sub-Q can be reused in situations where type qualifiers naturally arise---in reference immutability, function colouring, and capture checking. Finally, we re-examine other qualifier systems in the literature in light of the observations presented while developing System F-sub-Q.