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 is an area that is less examined. We explore how such a polymorphic system could arise by constructing a calculus System F<:Q which combines the higher-rank bounded polymorphism of System F<: with the theory of type qualifiers. We explore how the ideas used to System F<: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<:Q
Thu 24 OctDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:40 | Types and Gradual Typing 1OOPSLA 2024 at IBR West Chair(s): Fabian Muehlboeck Australian National University | ||
16:00 20mTalk | Intensional Functions OOPSLA 2024 Zachary Palmer Swarthmore College, Nathaniel Wesley Filardo Microsoft, Ke Wu Johns Hopkins University DOI | ||
16:20 20mTalk | Qualifying System F-sub OOPSLA 2024 Edward Lee University of Waterloo, Yaoyu Zhao University of Waterloo, Ondřej Lhoták University of Waterloo, James You University of Waterloo, Kavin Satheeskumar University of Waterloo, Jonathan Immanuel Brachthäuser University of Tübingen DOI | ||
16:40 20mTalk | Refinement Type Refutations OOPSLA 2024 Robin Webbers Vrije Universiteit Amsterdam, Klaus von Gleissenthall Vrije Universiteit Amsterdam, Ranjit Jhala UCSD DOI | ||
17:00 20mTalk | Type Inference Logics OOPSLA 2024 DOI | ||
17:20 20mTalk | Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs (SIGPLAN) OOPSLA 2024 Guannan Wei Inria/ENS; Tufts University, Oliver Bračevac EPFL, LAMP, Songlin Jia Purdue University, USA, Yuyan Bao Augusta University, Tiark Rompf Purdue University Link to publication |