一句话：构建 System F-sub-Q，将高阶有界多态与类型限定符理论结合，并用于引用不可变性、函数着色与捕获检查。
类型限定符（type qualifier）是一种轻量机制，可在既有类型系统上强制额外的程序不变式，其本质是受限的子类型。虽然类型限定符理论已较成熟并应用于多种语言，但关于类型限定符的多态性仍研究不足。本文构建演算 System F-sub-Q，将 System F-sub 的高阶有界多态与类型限定符理论结合起来，研究此类多态系统如何自然产生。作者进一步把构造该演算的思想复用到引用不可变性、函数着色和捕获检查等场景，并在 System F-sub-Q 的视角下重新审视文献中的其他限定符系统。
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.
@article{paperbot2536,
title = {Qualifying System F<sub><:</sub>: Some Terms and Conditions May Apply},
author = {Edward Lee and Yaoyu Zhao and Ondřej Lhoták and James You and Kavin Satheeskumar and Jonathan Immanuel Brachthäuser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649832}
}