Qualifying System F-sub

by Edward Lee, Yaoyu Zhao, Ondřej Lhoták, James You, Kavin Satheeskumar, and Jonathan Immanuel Brachthäuser

In Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2024.

This publication is related to the Type- and Effect Systems research project.

Abstract

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

Citation as BibTeX

@inproceedings{lee24qualifying,
  author = {Lee, Edward and Zhao, Yaoyu and Lhoták, Ondřej and You, James and Satheeskumar, Kavin and Brachthäuser, Jonathan Immanuel},
  title = {Qualifying System F-sub},
  techreport = {https://arxiv.org/abs/2311.07480},
  booktitle = {Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA)},
  year = {2024}
}