by Ed­ward Lee, Yaoyu Zhao, Ondřej Lhoták, James You, Kavin Satheesku­mar, and Jonathan Im­manuel Brachthäuser

In Pro­ceed­ings of the In­ter­na­tional Con­fer­ence on Ob­ject-Ori­ented Pro­gram­ming, Sys­tems, Lan­guages and Ap­pli­ca­tions (OOP­SLA), 2024.

This pub­li­ca­tion is re­lated to the Type- and Ef­fect Sys­tems re­search pro­ject.

Ab­stract

Type qual­i­fiers offer a light­weight mech­a­nism for en­rich­ing ex­ist­ing type sys­tems to en­force ad­di­tional, de­sir­able, pro­gram in­vari­ants. They do so by of­fer­ing a re­stricted but ef­fec­tive form of sub­typ­ing. While the the­ory of type qual­i­fiers is well un­der­stood and pre­sent in many pro­gram­ming lan­guages today, poly­mor­phism over type qual­i­fiers is an area that is less ex­am­ined. We ex­plore how such a poly­mor­phic sys­tem could arise by con­struct­ing a cal­cu­lus Sys­tem F<:Q which com­bines the higher-rank bounded poly­mor­phism of Sys­tem F<: with the the­ory of type qual­i­fiers. We ex­plore how the ideas used to Sys­tem F<:Q can be reused in sit­u­a­tions where type qual­i­fiers nat­u­rally arise—in ref­er­ence im­mutabil­ity, func­tion colour­ing, and cap­ture check­ing. Fi­nally, we re-ex­am­ine other qual­i­fier sys­tems in the lit­er­a­ture in light of the ob­ser­va­tions pre­sented while de­vel­op­ing Sys­tem F<:Q