1

# Qualifying System $\texttt{F}_{\texttt{<:}}$

Edward Lee  0000-0001-7057-0912 Computer ScienceUniversity of Waterloo200
University Ave W.WaterlooONN2L 3G1Canada ,  Yaoyu Zhao  Computer
ScienceUniversity of Waterloo200 University Ave W.WaterlooONN2L 3G1Canada ,
Ondřej Lhoták  0000-0001-9066-1889 Computer ScienceUniversity of Waterloo200
University Ave W.WaterlooONN2L 3G1Canada ,  James You  0009-0000-5906-0305
Computer ScienceUniversity of Waterloo200 University Ave W.WaterlooONN2L
3G1Canada ,  Kavin Satheeskumar  0009-0002-1106-2429 Computer
ScienceUniversity of Waterloo200 University Ave W.WaterlooONN2L 3G1Canada and
Jonathan Brachthäuser  0000-0001-9128-0391 Computer ScienceUniversity of
TübingenSand 13TübingenBaWü72076Germany

(Date: January 2023)

###### 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 $\texttt{F}_{\texttt{<:Q}}$ which combines the higher-rank bounded
polymorphism of System $\texttt{F}_{\texttt{<:}}$ with the theory of type
qualifiers. We explore how the ideas used to construct System
$\texttt{F}_{\texttt{<: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
$\texttt{F}_{\texttt{<:Q}}$.

System $\texttt{F}_{\texttt{<:}}$, Type Qualifiers, Type Systems

††journal: PACMPL††journalvolume: 1††journalnumber: OOPSLA††article:
1††journalyear: 2018††publicationmonth: 1††copyright: none††ccs: Software and
its engineering General programming languages††ccs: Software and its
engineering Compilers

##  1\. Introduction

Static type systems classify the values a program reduces to. For example, the
signature of the function

⬇

def toLowerCase(in: String): String = { ... }

toLowerCase enforces that it takes in a String as an argument and returns a
String as a result. If strings are implemented as mutable heap objects, how
would we express the additional property that toLowerCase does not its mutate
its input?

There are at least two ways to address this. We can view the modification of
toLowerCase’s argument in as a property of toLowerCase or we can view
mutability as a property of the argument string in itself. The former
viewpoint leads to solutions like (co-)effect systems (Petricek et al., 2014)
that describe the relation of a function to the context it is called in. The
latter viewpoint, of viewing it as a property of the argument, leads to
systems that enrich the types of values with additional information. In this
paper, we adopt the latter view.

Type qualifiers by Foster et al. (1999) is one such system. In such a system,
we could qualify the type of toLowerCase’s argument with the type qualifier
const to express that toLowerCase cannot modify its argument. We may choose to
annotate its result with the type qualifier const to indicate that its result
is a const String which cannot be changed by toLowerCase’s caller.

⬇

def toLowerCase(in: const String): const String = {...}

The function toLowerCase now accepts an immutable String as an argument and
presumably returns a new String that is a copy of its argument except in
lowercase. More importantly, since the input string is qualified as const, we
know that this version toLowerCase cannot mutate the input string; for
example, such as calling a method like in.setCharAt(0, ’A’), which would
replace the character of index 0 of the string with the character A.

Perhaps this is too restrictive. After all, toLowerCase will allocate a new
String and does not impose invariants on it; its caller should be permitted to
mutate the value returned. We should instead annotate toLowerCase as follows,
with a mutable qualifier on its return value.

⬇

def toLowerCase(in: const String): mutable String = {...}

Subtyping naturally arises in this context—a mutable String can be a subtype
of const String; this change will not alter the semantics of existing calls to
toLowerCase to break.

Similarly, it would be impractical if toLowerCase only accepted immutable
Strings. After all, any operation one could perform on a immutable String one
should be semantically valid on a mutable String as well. Therefore a mutable
String should ideally be a subtype of const String. If we wanted to, we should
be to chain calls to toLowerCase!

⬇

toLowerCase(toLowerCase("HELLO␣WORLD")) == "hello␣world"

Foster et al. (1999) were the first to recognize this natural subtyping
relation induced by type qualifiers, which permitted type qualifiers to be
integrated easily into existing type systems with subtyping. Perhaps the most
well known qualifier is const. const is used to mark particular values as
read-only or immutable and it is found in many languages and language
extensions (Stroustrup, 2007; Bright et al., 2020; Tschantz and Ernst, 2005).
Other languages, such as OCaml and Rust, are exploring more exotic qualifiers
to encode properties like locality, linearity, exclusivity, and synchronicity
(Slater, 2023b, a; Wuyts et al., 2022). Qualifiers are so easy to use that
many type system extensions start as type qualifier annotations on existing
types; for Java there is a framework (Papi et al., 2008) for doing so, and it
has been used to model extensions to Java for checking nullability, energy
consumption, and determinism amongst others using type qualifiers.

While type qualifiers themselves are well-explored, qualifier polymorphism is
still understudied. Sometimes parametric polymorphism is not necessary when
subtyping is present. For example, the type signature that we gave to
toLowerCase, const String => mutable String is indeed the most permissive type
that may be assigned. In languages with subtyping, variables are only
necessary to relate types and qualifiers in both co- and contravariant
positions; otherwise we can use their respective type bounds (Dolan, 2016,
Chapter 4.2.1). For example, while we could have made toLowerCase polymorphic
using a qualifier variable Q over the immutability of its input, such a change
is unnecessary as we can simply replace Q with its upper bound const to arrive
at the monomorphic but equally general version of toLowerCase from above.

⬇

def toLowerCase[Q <: const](in: Q String): mutable String = {...}

However, variables are indeed necessary when relating types and qualifiers in
covariant positions to types and qualifiers in contravariant positions. For
example, consider a substring function. Which qualifiers should we assign its
arguments and return value?

⬇

def substring(in: ??? String, from: Int, to: Int): ??? String = {...}

Clearly a substring of an immutable string should itself be immutable, but
also a substring of a mutable string should be mutable as well. To express
this set of new constraints, we need parametric qualifier polymorphism.

⬇

def substring[Q <: const](in: Q String, from: Int, to: Int): Q String

We also need to consider how qualifier polymorphism interacts with type
polymorphism. For example, what should be the type of a function like slice,
which returns a subarray of an array? It needs to be parametric over the the
type of the elements stored in the array, where the element type itself could
be qualified. This raises the question—should type variables range over
unqualified types or both unqualified and qualified types? Foster’s original
system does not address this issue, and existing qualifier systems disagree on
what type variables range over and whether or not type variables can be
qualified at all. For reasons we will demonstrate later in Section 5, type
variables should range over unqualified types; to achieve polymorphism over
both types and qualifiers, we need both type variables and qualifier variables
for orthogonality.

⬇

def slice[Qa<:const, Qv<:const, T<:Any](in: Qa Array[Qv T]): Qa Array[Qv T]

Another underexplored area is that of merging type qualifiers, especially in
light of parametric qualifier polymorphism. For example, consider the type
qualifiers throws and noexcept, expressing that a function may throw an
exception or that it does not throw any exception at all. Without
polymorphism, it is easy to combine qualifiers. For example, a function like
combined, that calls both pure and exception-throwing functions should be
qualified with the union of the two qualifiers, throws, expressing that an
exception could be thrown from the calling function.

⬇

def pure() = 0 // (() => Unit) noexcept

def impure() = throw new Exception("Hello") // (() => Unit) throws

def combined() = { pure(); impure() } // (() => Unit) throws

Things are more complicated in the presence of qualifier parametric higher-
order functions, such as:

⬇

def compose[A,B,C,Qf,Qg](f: (A => B) Qf, g: (B => C) Qg)): (A => C) ???

= (x) => g(f(x))

What should be the qualifier on the return type (A => C) of the function?
Intuitively, if either f or g throws an exception, then the result of compose
should be qualified with throws, but if neither throws any exception, then the
composition should be qualified with noexcept. Ideally we would like some
mechanism for specifying the union of the qualifiers annotated on both f and
g.

⬇

def compose[A,B,C,Qf,Qg](f: (A => B) Qf, g: (B => C) Qg)): (A => C) {Qf | Qg}

Existing qualifier systems today have limited support for these use cases.
Foster et al. (1999)’s original system is limited to simple ML-style qualifier
polymorphism with no mechanism for specifying qualifier-polymorphic function
types, and has limited support for combining qualifiers. Systems that do
support explicit qualifier polymorphism like that of Gordon et al. (2012)
partially ignore the interaction between combinations of qualifier variables
and their bounds, or present application-specific subqualification semantics
seen in Boruch-Gruszecki et al. (2023) or Wei et al. (2023). Must this always
be the case? Is there something in common we can generalize and apply to give
a design recipe for designing qualifier systems with subqualification and
polymorphism?

We believe this does not need to be the case; we show that it is possible to
add qualifier polymorphism without losing the natural lattice structure of
type qualifiers, and that there is a natural way to reconcile type
polymorphism with qualifier polymorphism as well.

To illustrate these ideas, we start by first giving a design recipe for
constructing a qualifier-polymorphic enrichment System
$\texttt{F}_{\texttt{<:Q}}$ of System $\texttt{F}_{\texttt{<:}}$, much in the
same way Foster et al. (1999) gives a design recipe for adding qualifiers to a
base simply-typed lambda calculus. Our recipe constructs a calculus with the
following desirable properties:

  * •

Higher-rank qualifier and type polymorphism: We show how to add higher-rank
qualifier polymorphism to a system with higher-rank type polymorphism in
Section 2.3.

  * •

Natural subtyping with qualifier variables: We show that the subtyping that
type qualifiers induce extends naturally even when working with qualifier
variables. We achieve this by using the free lattice generated over the
original qualifier lattice. We illustrate these ideas, first in a simplified
context over a fixed two-point qualifier lattice in Section 2.3 and generalize
to an arbitrary bounded qualifier lattice in Section 2.6.

  * •

Easy meets and joins: As we generalize the notion of a qualifier to that of an
element from the free (qualifier) lattice, we recover the ability to combine
qualifiers using meets and joins.

Next, to demonstrate the applicability of our qualifier polymorphism design
recipe, we show how one can model three natural problems – reference
immutability, function colouring, and capture tracking, using the ideas used
to develop System $\texttt{F}_{\texttt{<:Q}}$ in Section 3. We then discuss
how type polymorphism can interact with qualifier polymorphism in Section 5 to
justify our design choices. We then re-examine a selection of other qualifier
systems in light of our observations developed in our free lattice-based
subqualification recipe in Section 6 to see how their subqualification rules
fit in our free lattice based design recipe. Finally, we close with a
discussion of other related work in Section 7.

Our soundness proofs are mechanized in the Coq proof assistant; details are
discussed in Section 4.

##  2\. Qualified Type Systems

In this section, we introduce System $\texttt{F}_{\texttt{<:Q}}$, a simple
calculus with support for qualified types as well as type- and qualifier
polymorphism. We start off with a brief explanation of what type qualifiers
are (Subsection 2.1), introduce System $\texttt{F}_{\texttt{<:Q}}$ (Subsection
2.3), and show that it satisfies the standard soundness theorems (Subsection
2.5).

###  2.1. A Simply-Qualified Type System

As Foster et al. (1999) observes, type qualifiers induce a simple, yet highly
useful form of subtyping on qualified types. Consider a qualifier like const,
which qualifies an existing type to be read-only. It comes equipped with a
dual qualifier mutable which qualifies an existing type to be mutable. The
type const T is a _supertype_ of mutable T, for all types T; a mutable value
can be used wherever an immutable value is expected. Other qualifier pairs
induce a _subtype_ , like noexcept and throws—it is sound to use a function
which throws no exception in a context which would handle exceptions. Figure 1
provides an overview of some qualifiers and describes which invariants they
model.

Qualifiers |  Description
---|---
mutable <: const |  Mutability; a mutable value could be used anywhere an immutable value is expected. A covariant qualifier, as mutable is often omitted.
noexcept <: throws |  Exception safety; a function which throws no exceptions can be called anywhere a function which throws could. A contravariant qualifier, as throws is often omitted. (Maurer, 2015)
sync <: async |  Synchronicity; a function which is synchronous and does not suspend can be called in contexts where a function which is asynchronus and suspends could. Covariant, as sync is assumed by default.
nonnull <: nullable |  Nullability; a value which is guaranteed not to be null can be used in a context which can deal with nullable values. Covariant, in systems with this qualifier – most values ought not to be null.
Figure 1. Examples of type qualifiers

Often one of the two qualifiers is assumed by omission – for example mutable
and throws are often omitted; references are assumed to be mutable unless
otherwise specified, and similarly functions are assumed to possibly throw
exceptions as well. Qualifiers like const where the smaller qualifier is
omitted are positive, or covariant; by example, const String is a subtype of a
unqualified String. Conversely, qualifiers like noexcept are negative, or
contravariant; String => String noexcept is a subtype of String => String.

###  2.2. Qualifying a Language

The observation that qualifiers induce subtyping relationships allows language
designers to seamlessly integrate support for type qualifiers into existing
languages with subtyping. As Foster et al. (1999) point out, these qualifiers
embed into a qualifier lattice structure $\mathcal{L}$, and they give a design
recipe for enriching an existing type system with support for type qualifiers.

  1. (1)

First, embed qualifiers into a lattice $\mathcal{L}$. For example, const and
mutable embed into a two-point lattice, where const is $\top$ and mutable is
$\bot$. Other example qualifiers (and their embeddings) are described in
Figure 1.

  2. (2)

Second, extend the type system so that it operates on qualified types – a pair
$\\{{l}\\}~{}{T}$ where $l$ is a qualifier lattice element and $T$ a base type
from the original system. This is done in two steps.

  3. (3)

Embed qualifiers into the subtyping system. Typically, for two qualified types
$\\{{l_{1}}\\}~{}{T_{1}}$ and $\\{{l_{2}}\\}~{}{T_{2}}$ such that
$l_{1}\sqsubseteq l_{2}$ and $T_{1}~{}\texttt{<:}~{}T_{2}$ one will add the
subtyping rule
$\\{{l_{1}}\\}~{}{T_{1}}~{}\texttt{<:}~{}\\{{l_{2}}\\}~{}{T_{2}}$.

  4. (4)

Add rules for introducing qualifiers, typically in the introduction forms for
typing values.

  5. (5)

Finally, augment the other typing rules, typically elimination forms, so that
qualifiers are properly accounted for. One may also additionally add an
assertion rule for statically checking qualifiers as well.

###  2.3. Higher-rank Polymorphism

Foster’s original work allows one to add qualifiers to an existing type
system. As we discussed earlier, we want more, though:

  1. (1)

Qualifier Polymorphism: Certain functions ought to be polymorphic in the
qualifiers they expect. For example, from our introduction, we should be able
to express a substring function which is polymorphic in the mutability of the
string passed to it. While this is easy enough, as Foster et al. (1999) shows,
the interaction of lattice operations with qualifier variables is not so easy,
as we discuss below.

  2. (2)

Merging Qualifiers: We often need to merge qualifiers when constructing more
complicated values. Merging is easy when working with a lattice; we can just
take the lattice’s underlying join ($\sqcup$) or meet ($\sqcap$) operation.
But how do we reason about meets or joins of qualifier variables? For example,
in a noexcept qualifier system we should be able to collapse the qualifier on
the result of a function like twice which composes a function with itself from
$\hbox{\pagecolor{qualifier-blue-
bg}\color[rgb]{0.17578125,0.37109375,0.52734375}\definecolor[named]{pgfstrokecolor}{rgb}{0.17578125,0.37109375,0.52734375}{\tt
Q}}\sqcup\hbox{\pagecolor{qualifier-blue-
bg}\color[rgb]{0.17578125,0.37109375,0.52734375}\definecolor[named]{pgfstrokecolor}{rgb}{0.17578125,0.37109375,0.52734375}{\tt
Q}}$ to just Q; the result of twice throws if f throws or if f throws, which
is namely just if f throws.

⬇

def twice[A, Q](f: (A => A) Q): (A => A) Q = compose(f, f)

To achieve this, we need to extend qualifiers from just elements of a two-
point lattice, as in Foster et al. (1999), to formulas over lattices which can
involve qualifier variables in addition to elements of the original lattice.
Moreover, we would like to relate these formulas as well.

As Whitman (1941) observed, there is a lattice which encodes these relations
over these lattice formulas, namely, the free lattice constructed over the
original qualifier lattice. Free lattices capture exactly the lattice formulas
inequalities that are true in every lattice; given two lattice formulas over a
set of variables $f_{1}[\overline{X}]\sqsubseteq f_{2}[\overline{X}]$ in the
free lattice, $f_{1}[\overline{X}\to\overline{L}]\sqsubseteq
f_{2}[\overline{X}\to\overline{L}]$ in every lattice $\mathcal{L}$ and
instantiation $\overline{L}$ of the variables in $\overline{X}$ to elements of
$\mathcal{L}$.

It should not be surprising to see free lattices here; as Dolan (2016, Chapter
3) observed, free lattices can be used to model subtyping lattices with
unions, intersections, and variables as well. This allows us to generalize
Foster et al. (1999)’s recipe for qualifying types. Instead of qualifying
types by elements of the qualifier lattice, we qualify types by elements of
the free lattice generated over that base qualifier lattice, and we support
qualifier polymorphism explicitly with bounds following System
$\texttt{F}_{\texttt{<:}}$ instead of implicitly at prenex position with
constraints as Foster et al. (1999) do.

###  2.4. System $\texttt{F}_{\texttt{<:Q}}$

$\begin{array}[t]{rll@{\hspace{4mm}}l}\\\ s,t&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Terms}}\\\ &|&\hbox{\pagecolor{light-
gray}$\displaystyle\lambda({x})_{P}.{t}$}\hfil\hskip 11.38109pt&\mbox{term
abstraction}\\\ &|&x\hfil\hskip 11.38109pt&\mbox{term variable}\\\
&|&{s}({t})\hfil\hskip 11.38109pt&\mbox{application}\\\
&|&\hbox{\pagecolor{light-
gray}$\displaystyle\Lambda({X}~{}\texttt{<:}~{}{S})_{P}.{t}$}\hfil\hskip
11.38109pt&\mbox{type abstraction}\\\ &|&\hbox{\pagecolor{light-
gray}$\displaystyle\Lambda({Y}~{}\texttt{<:}~{}{Q})_{P}.{t}$}\hfil\hskip
11.38109pt&\mbox{qualifier abstraction}\\\ &|&{s}[{S}]\hfil\hskip
11.38109pt&\mbox{type application}\\\ &|&\hbox{\pagecolor{light-
gray}$\displaystyle{s}\\{\\!\\!\\{{Q}\\}\\!\\!\\}$}\hfil\hskip
11.38109pt&\mbox{qualifier application}\\\\[6.0pt] \Gamma&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Environment}}\\\ &|&\cdot\hfil\hskip
11.38109pt&\mbox{empty}\\\ &|&\Gamma,~{}x:T\hfil\hskip 11.38109pt&\mbox{term
binding}\\\ &|&\Gamma,~{}X<:S\hfil\hskip 11.38109pt&\mbox{type binding}\\\
&|&\Gamma,~{}\hbox{\pagecolor{light-gray}$\displaystyle Y<:Q$}\hfil\hskip
11.38109pt&\mbox{qualifier binding}\\\ \end{array}$

$\begin{array}[t]{rll@{\hspace{4mm}}l}\\\ S&::=&\hfil\hskip
11.38109pt&\mbox{{\bf{Simple Types}}}\\\ &|&\top\hfil\hskip
11.38109pt&\mbox{top type}\\\ &|&{T_{1}}\to{T_{2}}\hfil\hskip
11.38109pt&\mbox{function type}\\\ &|&X\hfil\hskip 11.38109pt&\mbox{type
variable}\\\ &|&\forall({X}~{}\texttt{<:}~{}{S}).{T}\hfil\hskip
11.38109pt&\mbox{for-all type}\\\ &|&\hbox{\pagecolor{light-
gray}$\displaystyle\forall({Y}~{}\texttt{<:}~{}{Q}).{T}$}\hfil\hskip
11.38109pt&\mbox{qualifier for-all type}\\\\[6.0pt] T&::=&\hfil\hskip
11.38109pt&\mbox{{\bf{Qualified Types}}}\\\ &|&\hbox{\pagecolor{light-
gray}$\displaystyle\\{{Q}\\}~{}{S}$}\hfil\hskip 11.38109pt&\mbox{qualified
type}\\\\[6.0pt] P,Q,R&::=&\hfil\hskip 11.38109pt&\mbox{{\bf{Qualifiers}}}\\\
&|&\top,\bot\hfil\hskip 11.38109pt&\mbox{Top and bottom}\\\ &|&Y\hfil\hskip
11.38109pt&\mbox{Qualifier variables}\\\ &|&Q\wedge R~{}|~{}Q\vee R\hfil\hskip
11.38109pt&\mbox{Meets and joins}\\\\[6.0pt] \end{array}$

$\begin{array}[t]{rll@{\hspace{4mm}}l}v&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Runtime Values}}\\\ &|&\lambda({x})_{P}.{t}\hfil\hskip
11.38109pt&\\\ &|&\Lambda({X}~{}\texttt{<:}~{}{S})_{P}.{t}\hfil\hskip
11.38109pt\\\ &|&\Lambda({Y}~{}\texttt{<:}~{}{Q})_{P}.{t}\hfil\hskip
11.38109pt\end{array}$

$\begin{array}[t]{rll@{\hspace{4mm}}l}C&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Concrete Qualifiers}}\\\ &|&\top\mbox{ or
}\bot\hfil\hskip 11.38109pt&\mbox{two-point lattice elements}\end{array}$

Lattice facts reminder: $\bot\sqsubseteq\bot$, $\bot\sqsubseteq\top$, and
$\top\sqsubseteq\top$. $\top\sqcap C=C$, $\top\sqcup C=\top$, $\bot\sqcap
C=\bot$, and $\bot\sqcup C=C$.

Figure 2. The syntax of System $\texttt{F}_{\texttt{<:Q}}$. Qualified
differences to System $\texttt{F}_{\texttt{<:}}$ highlighted in grey.

We are now ready to present our recipe by constructing System
$\texttt{F}_{\texttt{<:Q}}$, a qualified extension of System
$\texttt{F}_{\texttt{<:}}$ with support for type qualifiers, polymorphism over
type qualifiers, as well as meets ($Q\wedge R$) and joins ($Q\vee R$) over
qualifiers. We start by constructing a simplified version of System
$\texttt{F}_{\texttt{<:Q}}$ which models a free lattice over a two-point
qualifier lattice to illustrate our recipe.

#### Assigning Qualifiers

In System $\texttt{F}_{\texttt{<:Q}}$ we qualify types with the free lattice
generated over a base two-point lattice with $\top$ and $\bot$, but provide no
interpretation of $\top$ and $\bot$ as System $\texttt{F}_{\texttt{<:Q}}$ is
only a base calculus.

#### Syntax

Figure 2 presents the syntax of System $\texttt{F}_{\texttt{<:Q}}$, with
additions over System $\texttt{F}_{\texttt{<:}}$ highlighted in grey. Type
qualifiers $Q$ not only include $\top$ and $\bot$ as they would be in Foster
et al. (1999)’s original system. Here, in addition we support _qualifier
variables_ $Y$, as well as meets and joins over qualifiers. Type variables
support polymorphism over unqualified types. To support qualifier
polymorphism, we add a new qualifier for-all form
$\forall({Y}~{}\texttt{<:}~{}{Q}).{T}$. Similarly, on the term-level we add
qualifier abstraction $\Lambda({Y}~{}\texttt{<:}~{}{Q})_{P}.{t}$ and qualifier
application ${s}\\{\\!\\!\\{{Q}\\}\\!\\!\\}$.

To ensure that qualifiers have some runtime semantics in our base calculus, we
tag values with a qualifier expression $P$ denoting the qualifier that value
should be typed at and we add support for asserting as well as upcasting
qualifier tags, following Foster et al. (1999, Section 2.2). While System
$\texttt{F}_{\texttt{<:Q}}$ does not provide a default tag for values,
negative (or contravariant) qualifiers like noexcept would inform a default
qualifier tag choice of $\top$ – by default, functions are assumed to throw –
and positive (or covariant) qualifiers like const would inform a default
qualifier tag choice of $\bot$ – by default, in mutable languages, values
should be mutable. Put simply, the default value tag should correspond to the
default, omitted, qualifier.

Evaluation for System $\texttt{F}_{\texttt{<:Q}}$ $s\;\longrightarrow\;t$ and
$\operatorname{\texttt{eval}}{Q}$

$\displaystyle\begin{array}[]{@{}c@{}}{(\lambda({x})_{P}.{t})}({s})\;\longrightarrow\;t[x\mapsto
s]\end{array}$ (beta-v)

$\displaystyle\begin{array}[]{@{}c@{}}{(\Lambda({X}~{}\texttt{<:}~{}{S})_{P}.{t})}[{S^{\prime}}]\;\longrightarrow\;t[X\mapsto
S^{\prime}]\end{array}$ (beta-T)

$\displaystyle\begin{array}[]{@{}c@{}}{(\Lambda({Y}~{}\texttt{<:}~{}{Q})_{P}.{t})}\\{\\!\\!\\{{Q^{\prime}}\\}\\!\\!\\}\;\longrightarrow\;t[X\mapsto
Q^{\prime}]\end{array}$ (beta-Q)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}v\mbox{ tagged with
}P\quad\quad\operatorname{\texttt{eval}}(P)\sqsubseteq\operatorname{\texttt{eval}}(Q)\end{array}}{\begin{array}[]{@{}c@{}}\operatorname{\texttt{upqual}}P~{}v\;\longrightarrow\;v\mbox{
retagged with }Q\end{array}}$ (upqual)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}v\mbox{ tagged with
}P\quad\quad\operatorname{\texttt{eval}}(P)\sqsubseteq\operatorname{\texttt{eval}}(Q)\end{array}}{\begin{array}[]{@{}c@{}}\operatorname{\texttt{assert}}P~{}v\;\longrightarrow\;v\end{array}}$
(assert)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}s\;\longrightarrow\;t\end{array}}{\begin{array}[]{@{}c@{}}E[s]\;\longrightarrow\;E[t]\end{array}}$
(context)

$\begin{array}[]{lcll}E&::=&\mbox{\bf{Evaluation Context}}&\\\ &|&[]\\\
&|&E(t)~{}|~{}v(E)\\\ &|&E[S]~{}|~{}E[Q]\\\
&|&\operatorname{\texttt{upqual}}P~{}E\\\
&|&\operatorname{\texttt{assert}}P~{}E\end{array}$

$\begin{array}[t]{rlll}\\\
\operatorname{\texttt{eval}}(Q)&::=&&\mbox{\bf{Partial Qualifier
Evaluation}}\\\ &|~{}C&=>&C\\\ &|~{}Q\wedge
R&=>&\operatorname{\texttt{eval}}(Q)\sqcap\operatorname{\texttt{eval}}(R)\\\
&|~{}Q\vee
R&=>&\operatorname{\texttt{eval}}(Q)\sqcup\operatorname{\texttt{eval}}(R)\\\
&|~{}\\_&=>&\mbox{nothing, otherwise.}\end{array}$

Figure 3. Reduction rules for System $\texttt{F}_{\texttt{<:Q}}$

#### Semantics

The evaluation rules of System $\texttt{F}_{\texttt{<:Q}}$ (defined in Figure
3) are largely unchanged from System $\texttt{F}_{\texttt{<:}}$. To support
qualifier polymorphism we add the rule (beta-Q) for reducing applications of a
qualifier abstraction to a type qualifier expression. Finally, to ensure that
qualifiers have some runtime semantics even in our base calculus we add the
rules (upqual) and (assert) for asserting and upcasting qualifier tags: they
coerce qualifier expressions to concrete qualifiers when possible and ensure
that the concrete qualifiers are compatible before successfully reducing.

#### Subqualification

Subqualification for System $\texttt{F}_{\texttt{<:Q}}$ $\Gamma\vdash
Q~{}\texttt{<:}~{}R$

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}\top\end{array}$ (sq-top)

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash\bot~{}\texttt{<:}~{}Q\end{array}$
(sq-bot)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}R_{1}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}R_{1}\vee R_{2}\end{array}}$ (sq-join-intro-1)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}R_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}R_{1}\vee R_{2}\end{array}}$ (sq-join-intro-2)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
R_{1}~{}\texttt{<:}~{}Q\quad\quad\Gamma\vdash
R_{2}~{}\texttt{<:}~{}Q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
R_{1}\vee R_{2}~{}\texttt{<:}~{}Q\end{array}}$ (sq-join-elim)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
R_{1}~{}\texttt{<:}~{}Q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
R_{1}\wedge R_{2}~{}\texttt{<:}~{}Q\end{array}}$ (sq-meet-elim-1)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
R_{2}~{}\texttt{<:}~{}Q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
R_{1}\wedge R_{2}~{}\texttt{<:}~{}Q\end{array}}$ (sq-meet-elim-2)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}R_{1}\quad\quad\Gamma\vdash
Q~{}\texttt{<:}~{}R_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}R_{1}\wedge R_{2}\end{array}}$ (sq-meet-intro)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}Y~{}\texttt{<:}~{}Q\in\Gamma\quad\quad\Gamma\vdash
Q~{}\texttt{<:}~{}R\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
Y~{}\texttt{<:}~{}R\end{array}}$ (sq-var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}Y~{}\texttt{<:}~{}Q\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
Y~{}\texttt{<:}~{}Y\end{array}}$ (sq-refl-var)

Figure 4. Subqualification rules of System $\texttt{F}_{\texttt{<:Q}}$.

Figure 4 captures the free lattice structure of the qualifiers of System
$\texttt{F}_{\texttt{<:Q}}$ with a subqualification judgment $\Gamma\vdash
Q~{}\texttt{<:}~{}R$ to make precise the partial order between two lattice
formulas in a free lattice. This basic structure should appear familiar—it is
a simplified subtyping lattice. It should not be surprising that this
construction gives rise to the free lattice, though we make this property
explicit in supplementary material. One can use this structure to deduce
desirable subqualification judgments; for an environment
$\Gamma=[X~{}\texttt{<:}~{}A,Y~{}\texttt{<:}~{}B,A~{}\texttt{<:}~{}\top,B~{}\texttt{<:}~{}\top]$,
we can show that $X\vee Y~{}\texttt{<:}~{}A\vee B$, using the following rule
applications:

$\displaystyle X<:A\vee B$ by (sq-join-intro-1) $\displaystyle Y<:A\vee B$ by
(sq-join-intro-2) $\displaystyle X\vee Y<:A\vee B$ by (sq-join-elim)

#### Subtyping

Subtyping for System $\texttt{F}_{\texttt{<:Q}}$ $\Gamma\vdash
S_{1}~{}\texttt{<:}~{}S_{1}$ and $\Gamma\vdash T_{1}~{}\texttt{<:}~{}T_{2}$

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash
S~{}\texttt{<:}~{}\top\end{array}$ (sub-top)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}X\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
X~{}\texttt{<:}~{}X\end{array}}$ (sub-refl-svar)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}X~{}\texttt{<:}~{}S_{1}\in\Gamma\quad\quad\Gamma\vdash
S_{1}~{}\texttt{<:}~{}S_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
X~{}\texttt{<:}~{}S_{2}\end{array}}$ (sub-svar)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q_{1}~{}\texttt{<:}~{}Q_{2}\quad\quad\Gamma\vdash
S_{1}~{}\texttt{<:}~{}S_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\\{{Q_{1}}\\}~{}{S_{1}}~{}\texttt{<:}~{}\\{{Q_{2}}\\}~{}{S_{2}}\end{array}}$
(sub-qtype)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
T_{1}~{}\texttt{<:}~{}T_{2}\quad\quad\Gamma\vdash
T_{3}~{}\texttt{<:}~{}T_{4}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{T_{1}}\to{T_{3}}~{}\texttt{<:}~{}{T_{2}}\to{T_{4}}\end{array}}$
(sub-arrow)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
S_{2}~{}\texttt{<:}~{}S_{1}\quad\quad\Gamma,X~{}\texttt{<:}~{}S_{1}\vdash
T_{1}~{}\texttt{<:}~{}T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\forall({X}~{}\texttt{<:}~{}{S_{1}}).{T_{1}}~{}\texttt{<:}~{}\forall({X}~{}\texttt{<:}~{}{S_{2}}).{T_{2}}\end{array}}$
(sub-all)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q_{2}~{}\texttt{<:}~{}Q_{1}\quad\quad\Gamma,Y~{}\texttt{<:}~{}Q_{1}\vdash
T_{1}~{}\texttt{<:}~{}T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\forall({Y}~{}\texttt{<:}~{}{Q_{1}}).{T_{1}}~{}\texttt{<:}~{}\forall({Y}~{}\texttt{<:}~{}{Q_{2}}).{T_{2}}\end{array}}$
(sub-qall)

Figure 5. Subtyping rules of System $\texttt{F}_{\texttt{<:Q}}$.

System $\texttt{F}_{\texttt{<:Q}}$ inherits most of its rules for subtyping
from System $\texttt{F}_{\texttt{<:}}$, with two changes made (Figure 5). The
additional rule (sub-qall) handles subtyping for qualifier abstractions, and
rule (sub-qtype) handles subtyping for qualified types. All other rules remain
unchanged, except that rules (sub-arrow), (sub-all), and (sub-qall) are
updated to operate on qualified types $T$ (instead of simple types $S$).

#### Typing

Typing for System $\texttt{F}_{\texttt{<:Q}}$ $\Gamma\vdash t:T$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:T\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
x:T\end{array}}$ (var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,x:T_{1}\vdash
t:T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\lambda({x})_{P}.{t}:\\{{\hbox{\pagecolor{light-
gray}$\displaystyle P$}}\\}~{}{{T_{1}}\to{T_{2}}}\end{array}}$ (abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,X~{}\texttt{<:}~{}S\vdash
t:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\Lambda({X}~{}\texttt{<:}~{}{S})_{P}.{t}:\\{{\hbox{\pagecolor{light-
gray}$\displaystyle
P$}}\\}~{}{\forall({X}~{}\texttt{<:}~{}{S}).{T}}\end{array}}$ (t-abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,X~{}\texttt{<:}~{}S\vdash
t:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\Lambda({Y}~{}\texttt{<:}~{}{Q})_{P}.{t}:\\{{\hbox{\pagecolor{light-
gray}$\displaystyle
P$}}\\}~{}{\forall({Y}~{}\texttt{<:}~{}{Q}).{T}}\end{array}}$ (q-abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
t:\\{{Q}\\}~{}{S}\quad\quad\Gamma\vdash
Q~{}\texttt{<:}~{}P\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\operatorname{\texttt{assert}}P~{}t:\\{{Q}\\}~{}{S}\end{array}}$
(typ-assert)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
t:\\{{Q}\\}~{}{{T_{1}}\to{T_{2}}}\quad\quad\Gamma\vdash
s:T_{1}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{t}({s}):T_{2}\end{array}}$
(app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
t:\\{{Q}\\}~{}{\forall({X}~{}\texttt{<:}~{}{S}).{T}}\quad\quad\Gamma\vdash
S^{\prime}~{}\texttt{<:}~{}S\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{t}[{S^{\prime}}]:T[X\mapsto
S^{\prime}]\end{array}}$ (t-app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
t:\\{{R}\\}~{}{\forall({Y}~{}\texttt{<:}~{}{Q}).{T}}\quad\quad\Gamma\vdash
Q^{\prime}~{}\texttt{<:}~{}Q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{t}\\{\\!\\!\\{{Q^{\prime}}\\}\\!\\!\\}:T[Y\mapsto
Q^{\prime}]\end{array}}$ (q-app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
s:T_{1}\quad\quad\Gamma\vdash
T_{1}~{}\texttt{<:}~{}T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
s:T_{2}\end{array}}$ (sub)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
t:\\{{Q}\\}~{}{S}\quad\quad\Gamma\vdash
Q~{}\texttt{<:}~{}P\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\operatorname{\texttt{upqual}}P~{}t:\\{{P}\\}~{}{S}\end{array}}$
(typ-upqual)

Figure 6. Typing rules for System $\texttt{F}_{\texttt{<:Q}}$

Finally, Figure 6 defines the typing rules of System
$\texttt{F}_{\texttt{<:Q}}$. The typing judgment assigns qualified types $T$
to expressions, and can be viewed as $\Gamma\vdash t:\\{{Q}\\}~{}{S}$. As
System $\texttt{F}_{\texttt{<:Q}}$ does not assign an interpretation to
qualifiers, the introduction rules for typing values, (abs), (t-abs), and
(q-abs), simply introduce qualifiers by typing values with their tagged
qualifier, and the elimination rules remain unmodified. The only (new)
elimination rules which deal with qualifiers are the new rules (typ-assert)
and (typ-upqual), which check that their argument is properly qualified. We
additionally add (q-abs) and (q-app) to support qualifier polymorphism.
Besides these changes, the typing rules immediately carry over from System
$\texttt{F}_{\texttt{<:}}$.

###  2.5. Metatheory

System $\texttt{F}_{\texttt{<:Q}}$ satisfies the standard progress and
preservation theorems.

###### Theorem 2.1 (Preservation).

Suppose $\Gamma\vdash s:T$, and $s\;\longrightarrow\;t$. Then $\Gamma\vdash
t:T$ as well.

###### Theorem 2.2 (Progress).

Suppose $\varnothing\vdash s:T$. Then either $s$ is a value, or
$s\;\longrightarrow\;t$ for some term $t$.

While System $\texttt{F}_{\texttt{<:Q}}$ does not place any interpretation on
qualifiers outside of $\operatorname{\texttt{upqual}}$ and
$\operatorname{\texttt{assert}}$, such a system can already be useful. For
one, the static type of a value will always be greater than the tag annotated
on it and this correspondence is preserved through reduction by progress and
preservation. This property can already be used to enforce safety constraints.
For example, as Foster et al. (1999) point out, one can use a negative type
qualifier sorted to distinguish between sorted and unsorted lists. By default
most lists would be tagged at $\top$, marking them as unsorted lists. A
function like merge, though, which merges two sorted lists into a third sorted
list, would expect two $\bot$-tagged lists, $\operatorname{\texttt{assert}}$
that they are actually $\bot$-tagged, and produce a $\bot$-tagged list as
well. While this scheme does not ensure that all $\bot$-tagged lists are
sorted, so long as programmers are careful to ensure that they never construct
explicitly $\bot$-tagged unsorted lists, they can ensure that functions which
expect sorted lists are actually passed sorted lists.

###  2.6. Generalizing Qualifiers to General Lattices

Qualifiers often come in more complicated lattices: for example, protection
rings (Karger and Herbert, 1984) induce a countable lattice, and combinations
of binary qualifiers induce a product lattice. Now, we show how we can tweak
the recipe used to construct System $\texttt{F}_{\texttt{<:Q}}$ for two-point
lattices to support general (countable, bounded) qualifier lattices
$\mathcal{L}$ as well.

$\begin{array}[t]{rll@{\hspace{4mm}}l}\\\ P,Q,R&::=&\hfil\hskip
11.38109pt&\mbox{{\bf{Qualifiers in extended System
$\texttt{F}_{\texttt{<:Q}}$}}}\\\ &|&\hbox{\pagecolor{light-
gray}$\displaystyle l$}\hfil\hskip 11.38109pt&\mbox{Base lattice elements
$l\in L$}\\\ &|&Y\hfil\hskip 11.38109pt&\mbox{Qualifier variables}\\\
&|&Q\wedge R~{}|~{}Q\vee R\hfil\hskip 11.38109pt&\mbox{Meets and
joins}\\\\[6.0pt] C&::=&\hfil\hskip 11.38109pt&\mbox{\bf{Concrete
Qualifiers}}\\\ &|&\hbox{\pagecolor{light-gray}$\displaystyle l$}\hfil\hskip
11.38109pt&\mbox{Base lattice elements $l\in L$}\end{array}$ Figure 7. The
syntax of System $\texttt{F}_{\texttt{<:Q}}$ extended over a bounded lattice
$\mathcal{L}$. Differences to System $\texttt{F}_{\texttt{<:Q}}$ highlighted
in grey.

Subqualification for System $\texttt{F}_{\texttt{<:Q}}$ over a lattice
$\mathcal{L}$ $\Gamma\vdash Q~{}\texttt{<:}~{}R$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}l_{1},l_{2}\in\mathcal{L}\quad\quad
l_{1}\sqsubseteq l_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
l_{1}~{}\texttt{<:}~{}l_{2}\end{array}}$ (sq-lift)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}Q^{\prime}\quad\quad\Gamma\vdash
l=\operatorname{\texttt{eval}}{Q^{\prime}}\quad\quad\Gamma\vdash
l~{}\texttt{<:}~{}R\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}R\end{array}}$ (sq-eval-elim)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}l\quad\quad\Gamma\vdash
l=\operatorname{\texttt{eval}}{Q^{\prime}}\quad\quad\Gamma\vdash
Q^{\prime}~{}\texttt{<:}~{}R\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
Q~{}\texttt{<:}~{}R\end{array}}$ (sq-eval-intro)

Figure 8. Extended sub-qualification rules for System
$\texttt{F}_{\texttt{<:Q}}$.

#### Syntax

The syntax changes needed to support this construction are listed in Figure 7.
Lattice elements are now generalized from $\top$ and $\bot$ to elements $l$
from our base lattice $\mathcal{L}$, but as $\mathcal{L}$ is bounded, note
that we still have distinguished elements $\top$ and $\bot$ in $\mathcal{L}$.

#### Subqualification

The subqualification changes needed to support this construction are listed in
Figure 8. These are exactly the rules needed to support the free lattice
construction over any arbritrary countable bounded lattice. Rule (sq-lift)
simply lifts the lattice order $\sqsubseteq$ that $\mathcal{L}$ is equipped
with up to the free lattice order defined by the subqualification lattice.
Rules (sq-eval-elim) and (sq-eval-intro) are a little more complicated,
though, but are necessary in order to relate textual meets and joins of
elements of the base lattice $\mathcal{L}$, like $l_{1}\vee l_{2}$, to their
actual meets and joins in the qualifier lattice, $l_{1}\sqcup l_{2}$. We would
expect that these two terms would be equivalent in the subqualification
lattice; namely, that $\Gamma\vdash l_{1}\vee
l_{2}~{}\texttt{<:}~{}l_{1}\sqcup l_{2}$ and that $\Gamma\vdash l_{1}\sqcup
l_{2}~{}\texttt{<:}~{}l_{1}\vee l_{2}$. However, without the two evaluation
rules (sq-eval-elim) and (sq-eval-intro) we would only be able to conclude
that $\Gamma\vdash l_{1}\vee l_{2}~{}\texttt{<:}~{}l_{1}\sqcup l_{2}$, but not
the other desired inequality $\Gamma\vdash l_{1}\sqcup
l_{2}~{}\texttt{<:}~{}l_{1}\vee l_{2}$.

To discharge this equivalence, (sq-eval-elim) and (sq-eval-intro) use
$\operatorname{\texttt{eval}}$ to simplify qualifier expressions. Again, it
should not be surprising that this gives rise to the free lattice of
extensions of $\mathcal{L}$, though we make this precise in supplementary
material.

#### Soundness

Like simple System $\texttt{F}_{\texttt{<:Q}}$, System
$\texttt{F}_{\texttt{<:Q}}$ extended over an bounded lattice $\mathcal{L}$
also satisfies the standard soundness theorems:

###### Theorem 2.3 (Preservation for Extended System
$\texttt{F}_{\texttt{<:Q}}$).

Suppose $\Gamma\vdash s:T$, and $s\;\longrightarrow\;t$. Then $\Gamma\vdash
t:T$ as well.

###### Theorem 2.4 (Progress for Extended System $\texttt{F}_{\texttt{<:Q}}$).

Suppose $\varnothing\vdash s:T$. Either $s$ is a value, or
$s\;\longrightarrow\;t$ for some term $t$.

However this construction while sound poses some difficulties. The
subqualification rules now need to handle transitivity through base lattice
elements, and these new rules are not syntax directed. It remains an open
question as to whether or not extended System $\texttt{F}_{\texttt{<:Q}}$
admits algorithmic subtyping rules, and we suspect the answer depends on the
structure of the base bounded qualifier lattice $\mathcal{L}$ being extended.

##  3\. Applications

Having introduced our design recipe by constructing System
$\texttt{F}_{\texttt{<:Q}}$ as a qualified extension of System
$\texttt{F}_{\texttt{<:}}$, we now study how our subqualification and
polymorphism recipe can be reused in three practical qualifier systems. For
brevity we will base our qualifier systems on System
$\texttt{F}_{\texttt{<:Q}}$ as it already provides rules and semantics for
typing, subqualification and qualifier polymorphism, which we modify below.

###  3.1. Reference Immutability

We start by examining one well-studied qualifier system, that of reference
immutability (Tschantz and Ernst, 2005; Huang et al., 2012). In this setting,
each (heap) reference can be either mutable or immutable. An immutable
reference cannot be used to mutate the value or any other values transitively
reached from it, so a value read through a readonly-qualified compound object
or reference is itself readonly as well. Mutable and immutable references can
coexist for the same value, so an immutable reference does not itself
guarantee that the value will not change through some other, mutable
reference. This is in contrast to the stronger guarantee of object
immutability, which applies to values, and ensures that a particular value
does not change through any of the references to it (Zibin et al., 2007).

Reference immutability systems have long been studied in various contexts
(Tschantz and Ernst, 2005; Huang et al., 2012; Zibin et al., 2007; Gordon et
al., 2012; Lee and Lhoták, 2023; Dort and Lhoták, 2020). Here, we show that we
can reuse our recipe to model reference immutability in a setting with higher
rank polymorphism and subtyping over both qualifiers and ground types, in a
calculus System $\texttt{F}_{\texttt{<:QM}}$.

#### Assigning Qualifiers

We need to define how qualifiers mutable and readonly are assigned to $\top$
and $\bot$ in System $\texttt{F}_{\texttt{<:QM}}$. Since a mutable reference
can always be used where a readonly reference is expected, we assign mutable
to $\bot$ and readonly to $\top$. This is reflected in Figure 9.

#### Syntax and Evaluation

Now we need to design syntax and reduction rules for references and immutable
references. We add support for references via $\operatorname{\texttt{box}}$
forms and we add rules for introducing and eliminating boxes. To distinguish
between mutable and immutable boxes, we reuse the qualifiers tagged on
values–values with tags $P$ that $\operatorname{\texttt{eval}}$ to $\bot$ are
mutable, whereas values with tags $P$ that otherwise evaluate to $\top$ are
mutable. One can explicitly mark a value immutable by
$\operatorname{\texttt{upqual}}$-ing to $\top$. The elimination form for
reading from a reference, (deref), ensures that a value read from a reference
tagged immutable, or at $\top$, remains immutable. This is reflected in the
updated operational semantics (Figure 10). Reduction now takes place over
pairs of terms and stores $\langle t,\sigma\rangle$; stores map locations $l$
to values.

$\begin{array}[t]{rll@{\hspace{4mm}}l}\\\ s,t&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Terms}}\\\ &\ldots\\\
&|&\operatorname{\texttt{box}}_{P}t\hfil\hskip 11.38109pt&\mbox{reference
cell}\\\ &|&\texttt{unbox}~{}s\hfil\hskip 11.38109pt&\mbox{deferencing}\\\
&|&\texttt{set-box!}~{}{s}~{}{t}\hfil\hskip 11.38109pt&\mbox{reference
update}\end{array}$

$\begin{array}[t]{rll@{\hspace{4mm}}l}\\\ S&::=&\hfil\hskip
11.38109pt&\mbox{{\bf{Types}}}\\\ &\ldots\\\
&|&\operatorname{\texttt{box}}S\hfil\hskip 11.38109pt&\mbox{reference
type}\\\\[6.0pt] P,Q,R&::=&\hfil\hskip 11.38109pt&\mbox{\bf{Qualifiers}}\\\
&\ldots&\hfil\hskip 11.38109pt&\mbox{as before, except:}\\\
&|&\operatorname{\texttt{readonly}}\hfil\hskip 11.38109pt&\mbox{const
qualifier (as $\top$)}\\\ &|&\operatorname{\texttt{mutable}}\hfil\hskip
11.38109pt&\mbox{non-const qualifier (as $\bot$)}\\\\[6.0pt] \end{array}$

$\begin{array}[t]{rll@{\hspace{4mm}}l}&&l\hfil\hskip
11.38109pt&\mbox{\bf{Location}}\\\\[6.0pt] s,t&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Runtime Terms}}\\\
&|&\operatorname{\texttt{box}}_{P}l\hfil\hskip 11.38109pt&\mbox{runtime
reference}\\\\[6.0pt] v&::=&\hfil\hskip 11.38109pt&\mbox{\bf{Runtime
Values}}\\\ &\ldots\\\ &|&\operatorname{\texttt{box}}_{P}l\hfil\hskip
11.38109pt\end{array}$

$\begin{array}[t]{rll@{\hspace{4mm}}l}\sigma&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Store}}\\\ &|&\cdot\hfil\hskip 11.38109pt&\mbox{empty}\\\
&|&\sigma,~{}l:v\hfil\hskip 11.38109pt&\mbox{cell $l$ with value
$v$}\\\\[6.0pt] \Sigma&::=&\hfil\hskip 11.38109pt&\mbox{\bf{Store
Environment}}\\\ &|&\cdot\hfil\hskip 11.38109pt&\mbox{empty}\\\
&|&\sigma,~{}l:T\hfil\hskip 11.38109pt&\mbox{cell binding}\end{array}$

Figure 9. The syntax of System $\texttt{F}_{\texttt{<:QM}}$.

Additional Evaluation Rules for System $\texttt{F}_{\texttt{<:QM}}$ $\langle
s,\sigma\rangle\;\longrightarrow\;\langle t,\sigma^{\prime}\rangle$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}l\notin\sigma\end{array}}{\begin{array}[]{@{}c@{}}\langle\operatorname{\texttt{box}}_{P}v,\sigma\rangle\;\longrightarrow\;\langle\operatorname{\texttt{box}}_{P}l,(\sigma,l:v)\rangle\end{array}}$
(ref-store)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}l:v\in\sigma\quad\quad v\mbox{
tagged with
}Q\end{array}}{\begin{array}[]{@{}c@{}}\langle\texttt{unbox}~{}\operatorname{\texttt{box}}_{P}l,\sigma\rangle\;\longrightarrow\;\langle
v\mbox{ retagged at }P\vee Q,\sigma\rangle\end{array}}$ (deref)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}l:v\in\sigma\quad\quad\operatorname{\texttt{eval}}(P)\sqsubseteq\bot\end{array}}{\begin{array}[]{@{}c@{}}\langle\texttt{set-
box!}~{}{(}~{}{\operatorname{\texttt{box}}}_{P}~{}l~{})~{}v^{\prime},\sigma\rangle\mapsto\langle
v,\sigma[l\mapsto v^{\prime}]\rangle\end{array}}$ (write-ref)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\langle
s,\sigma\rangle\;\longrightarrow\;\langle
t,\sigma^{\prime}\rangle\end{array}}{\begin{array}[]{@{}c@{}}\langle
E[s],\sigma\rangle\;\longrightarrow\;\langle
E[t],\sigma^{\prime}\rangle\end{array}}$ (context)

$\begin{array}[]{lcll}E&::=&\ldots&\mbox{{\bf Evaluation Context}}\\\
&|&\operatorname{\texttt{box}}_{P}E\\\ &|&\texttt{unbox}~{}E\\\
&|&\texttt{set-box!}~{}{E}~{}{~{}}t~{}|~{}\texttt{set-
box!}~{}{v}~{}{~{}}E\end{array}$

Figure 10. Reduction rules for System $\texttt{F}_{\texttt{<:QM}}$

#### Typing

Additional Typing and Runtime Typing for System $\texttt{F}_{\texttt{<:QM}}$
$\Gamma~{}|~{}\Sigma\vdash t:T$ and $\Gamma~{}|~{}\hbox{\pagecolor{light-
gray}$\displaystyle\Sigma$}\vdash\sigma$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}\Sigma\vdash
t:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}\Sigma\vdash\operatorname{\texttt{box}}_{P}t:\\{{P}\\}~{}{\operatorname{\texttt{box}}T}\end{array}}$
(ref-intro)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}l:T\in\Sigma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}\Sigma\vdash\operatorname{\texttt{box}}_{P}l:\\{{P}\\}~{}{\operatorname{\texttt{box}}T}\end{array}}$
(runtime-ref-intro)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}\Sigma\vdash
t:\\{{Q_{1}}\\}~{}{\operatorname{\texttt{box}}\\{{Q_{2}}\\}~{}{S}}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}\Sigma\vdash\texttt{unbox}~{}t:\\{{\hbox{\pagecolor{light-
gray}$\displaystyle Q_{1}\vee Q_{2}$}}\\}~{}{S}\end{array}}$ (ref-elim)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
s:\\{{\hbox{\pagecolor{light-
gray}$\displaystyle\operatorname{\texttt{mutable}}$}}\\}~{}{\operatorname{\texttt{box}}T}\quad\quad\Gamma\vdash
t:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\texttt{set-
box!}~{}{s}~{}{~{}}t:T\end{array}}$ (ref-update)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}dom(\sigma)=dom(\Sigma)\quad\quad\forall
l\in
dom(\Sigma),~{}\Gamma~{}|~{}\Sigma\vdash\sigma(l):\Sigma(l)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}\Sigma\vdash\sigma\end{array}}$
(store)

Figure 11. Typing rules for System $\texttt{F}_{\texttt{<:QM}}$; notable
changes highlighted in grey.

We now need to define new typing rules for reference forms and to possibly
adjust existing typing rules to account for our new runtime interpretation of
qualifiers. For this system, we only need to add typing rules, as shown in
Figure 11. To ensure immutability safety, the standard reference update
elimination form (ref-update) is augmented to check that a reference can only
be written to if and only if it can be typed as mutable
$\operatorname{\texttt{box}}{}$. Finally, the standard reference read
elimination form (ref-elim) is augmented to enforce that the mutability of the
value read from a reference is joined with the mutability of the reference
itself to ensure transitive immutability safety. Other than qualifiers, our
construction is completely standard; we merely add a store $\sigma$ and a
runtime store environment $\Sigma$ mapping store locations to types.

#### Metatheory

We can prove the standard soundness theorems without any special difficulty:

###### Theorem 3.1 (Preservation of System $\texttt{F}_{\texttt{<:QM}}$).

Suppose $\langle s,\sigma\rangle\;\longrightarrow\;\langle
t,\sigma^{\prime}\rangle$. If $\Gamma~{}|~{}\Sigma\vdash\sigma$ and
$\Gamma~{}|~{}\Sigma\vdash s:T$ for some type $T$, then there is some
environment extension $\Sigma^{\prime}$ of $\Sigma$ such that
$\Gamma~{}|~{}\Sigma^{\prime}\vdash\sigma^{\prime}$ and
$\Gamma~{}|~{}\Sigma^{\prime}\vdash t:T$.

###### Theorem 3.2 (Progress for System $\texttt{F}_{\texttt{<:QM}}$).

Suppose $\varnothing~{}|~{}\Sigma\vdash\sigma$ and $\varnothing,\Sigma\vdash
s:T$. Then either $s$ is a value or there is some $t$ and $\sigma^{\prime}$
such that $\langle s,\sigma\rangle\;\longrightarrow\;\langle
t,\sigma^{\prime}\rangle$.

With only progress and preservation, we can already state something meaningful
about the immutability safety of System $\texttt{F}_{\texttt{<:QM}}$: we know
that well-typed programs will not get stuck trying to write to a
sealed,$\bot$-tagged reference. Moreover, the typing rules, in particular
(ref-elim), give us our desired transitive immutability safety as well; values
read from a $\bot$-tagged value will remain $\bot$-tagged and therefore
immutable as well. In addition, as qualifier tags only affect reduction by
blocking reduction (that is, getting stuck) we almost directly recover full
immutability safety as well for free, by noting that references typed (by
subtyping) at readonly can be re-tagged at readonly as well without affecting
reduction, assuming the original program was well-typed.

###  3.2. Function Colouring

Function colouring (Nystrom, 2015) is another qualifier system. In this
setting, functions are qualified with a kind that indicates a colour for each
function, and there are restrictions on which other functions a function can
call depending on the colours of the callee and caller. For example, noexcept
and throws forms a function colouring system—functions qualified noexcept can
only call functions qualified noexcept. Another instantiation of this problem
is the use of the qualifiers sync and async in asynchronous programming.
async-qualified functions may call all functions but sync-qualified functions
may only call other sync-qualified functions. Polymorphism with function
colours is known to be painful (Nystrom, 2015). Consider a higher-order
function map:

⬇

def map[X, Y](l: List[X], f: (X => Y)) = ???

What should its colour be? The colour of a function like map depends on the
function f it is applying. Without a mechanism to express this dependency,
such as colour polymorphism, functions like map need to be implemented
twice—once for an async-qualified f, and once for a sync-qualified f.
Moreover, function colouring requires a mechanism for mixing colours! Consider
function composition:

⬇

def compose[A, B, C, D](f: A => B, g: C => D) = (x) => g(f(x))

The colour of the result of compose needs to be the join of the colours of f
and g. If either f or g are asynchronous then the result of compose is as
well, but if both f and g are synchronous then so should the result of
composing them. We now show how our recipe can be used to construct System
$\texttt{F}_{\texttt{<:QA}}$, a calculus that enforces these restrictions.

#### Assigning Qualifiers

Since a synchronous function can be called anywhere that an asynchronous
function could be, we assign the $\top$ qualifier to async and the $\bot$
qualifier to sync.

#### Syntax

$\begin{array}[t]{rll@{\hspace{4mm}}l}\\\ P,Q,R&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Qualifiers}}\\\ &\ldots&\hfil\hskip 11.38109pt&\mbox{as
before, except:}\\\ &|&\operatorname{\texttt{async}}~{}(\mbox{as
}\top)\hfil\hskip 11.38109pt&\mbox{async qualifier}\\\
&|&\operatorname{\texttt{sync}}~{}(\mbox{as }\bot)\hfil\hskip
11.38109pt&\mbox{sync qualifier}\\\\[6.0pt] \kappa&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Evaluation Context}}\\\ &|&[]\hfil\hskip 11.38109pt\\\
&|&f::\kappa\hfil\hskip 11.38109pt\\\\[6.0pt] \end{array}$

$\begin{array}[t]{rll@{\hspace{4mm}}l}\\\ f&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Evaluation Frames}}\\\ &|&\hbox{\pagecolor{light-
gray}$\displaystyle\operatorname{\texttt{barrier}}C$}\hfil\hskip
11.38109pt&\mbox{barrier}\\\ &|&\operatorname{\texttt{arg}}t\hfil\hskip
11.38109pt&\mbox{argument}\\\ &|&\operatorname{\texttt{app}}v\hfil\hskip
11.38109pt&\mbox{application}\\\ &|&\operatorname{\texttt{targ}}T\hfil\hskip
11.38109pt&\mbox{type application}\\\
&|&\operatorname{\texttt{qarg}}Q\hfil\hskip 11.38109pt&\mbox{qualifier
application}\\\\[6.0pt] \end{array}$

Figure 12. The syntax of System $\texttt{F}_{\texttt{<:QA}}$.

Figure 12 presents the modified syntax of System $\texttt{F}_{\texttt{<:QA}}$.
To keep track of the synchronicity a function term should run in we reuse the
tags already preset in values. An example of an asynchronous function term is
$\lambda({x})_{\tt{async}}.{\;x}$, and an example of a function that is
polymorphic in its qualifier is
$\Lambda({Y}~{}\texttt{<:}~{}{\tt{sync}})_{\tt{async}}.{\lambda({f})_{Y}.{\;f(1)}}$,
describing a function that should run in the same synchronicity context as its
argument $f$.

#### Evaluation

Evaluation for System $\texttt{F}_{\texttt{<:QA}}$
$\langle{c},{\kappa}\rangle\;\longrightarrow\;\langle{c^{\prime}},{\kappa^{\prime}}\rangle$

$\displaystyle\begin{array}[]{@{}c@{}}\langle{{s}({t})},{\kappa}\rangle\;\longrightarrow\;\langle{s},{\operatorname{\texttt{arg}}t::\kappa}\rangle\end{array}$
(cong-app)

$\displaystyle\begin{array}[]{@{}c@{}}\langle{v},{\operatorname{\texttt{app}}t::\kappa}\rangle\;\longrightarrow\;\langle{t},{\operatorname{\texttt{app}}v::\kappa}\rangle\end{array}$
(cong-arg)

$\displaystyle\begin{array}[]{@{}c@{}}\langle{{s}[{S}]},{\kappa}\rangle\;\longrightarrow\;\langle{s},{\operatorname{\texttt{targ}}S::\kappa}\rangle\end{array}$
(cong-tapp)

$\displaystyle\begin{array}[]{@{}c@{}}\langle{{s}\\{\\!\\!\\{{Q}\\}\\!\\!\\}},{\kappa}\rangle\;\longrightarrow\;\langle{s},{\operatorname{\texttt{qarg}}Q::\kappa}\rangle\end{array}$
(cong-qapp)

$\displaystyle\begin{array}[]{@{}c@{}}\langle{v},{\operatorname{\texttt{barrier}}C::\kappa}\rangle\;\longrightarrow\;\langle{v},{\kappa}\rangle\end{array}$
(break-barrier)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}C\leq C_{i}\text{ for all
}\operatorname{\texttt{barrier}}~{}C_{i}\text{ frames on
}\kappa\quad\quad\operatorname{\texttt{eval}}{P}=C\end{array}}{\begin{array}[]{@{}c@{}}\langle{v},{\operatorname{\texttt{app}}\lambda({x})_{P}.{t}::\kappa}\rangle\;\longrightarrow\;\langle{t[x\mapsto
v]},{\operatorname{\texttt{barrier}}C::\kappa}\rangle\end{array}}$ (reduce-
app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}C\leq C_{i}\text{ for all
}\operatorname{\texttt{barrier}}~{}C_{i}\text{ frames on
}\kappa\quad\quad\operatorname{\texttt{eval}}{P}=C\end{array}}{\begin{array}[]{@{}c@{}}\langle{\Lambda({X}~{}\texttt{<:}~{}{S})_{P}.{t}},{\operatorname{\texttt{targ}}S^{\prime}::\kappa}\rangle\;\longrightarrow\;\langle{t[X\mapsto
S^{\prime}]},{\operatorname{\texttt{barrier}}C::\kappa}\rangle\end{array}}$
(reduce-tapp)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}C\leq C_{i}\text{ for all
}\operatorname{\texttt{barrier}}~{}C_{i}\text{ frames on
}\kappa\quad\quad\operatorname{\texttt{eval}}{P}=C\end{array}}{\begin{array}[]{@{}c@{}}\langle{\Lambda({Y}~{}\texttt{<:}~{}{Q})_{P}.{t}},{\operatorname{\texttt{qarg}}Q^{\prime}::\kappa}\rangle\;\longrightarrow\;\langle{t[Y\mapsto
Q^{\prime}]},{\operatorname{\texttt{barrier}}C::\kappa}\rangle\end{array}}$
(reduce-qapp)

Figure 13. Operational Semantics (CK-style) for System
$\texttt{F}_{\texttt{<:QA}}$

To model synchronicity safety, Figure 13 describes the operational semantics
of System $\texttt{F}_{\texttt{<:QA}}$ using Felleisen and Friedman
(1987)-style CK semantics, extended with special barrier frames installed on
the stack denoting the colour of the function that was called. When a function
is called, we place a barrier with the evaluated colour of the function
itself, and functions may only be called if the barriers on the stack are
compatible with the evaluated colour of the function being called—namely, an
asynchronous function can be called only if there are no barriers on the stack
marked synchronous. The other evaluation contexts are standard.

#### Typing

To guarantee soundness, Figure 14 endows the typing rules of System
$\texttt{F}_{\texttt{<:QA}}$ with modified rules for keeping track of the
synchronicity context that a function needs. We extend the typing rules with a
colour context $R$ to keep track of the synchronicity of the functions being
called. This colour context $R$ is simply a qualifier expression, and is
introduced by the introduction rules for typing abstractions by lifting the
qualifier tagged on those abstractions – see rules (A-abs), (A-t-abs), and
(A-q-abs). To ensure safety when applying functions in the elimination
(A-app), we check that the colour context is compatible with the type of the
function being called; subsumption in (A-sub-eff) allows functions to run if
the qualifiers do not exactly match but when the qualifier on the function is
subqualified by the colour context. The typing rules outside of manipulating
the context $R$ remain otherwise unchanged.

#### Metatheory

With all this, we can state and prove progress and preservation for System
$\texttt{F}_{\texttt{<:QA}}$.

###### Theorem 3.3 (Progress of System $\texttt{F}_{\texttt{<:QA}}$).

Suppose $\langle c,\kappa\rangle$ is a well-typed machine configuration. Then
either $c$ is a value and $k$ is the empty continuation, or there is a machine
state $\langle c^{\prime},\kappa^{\prime}\rangle$ that it steps to.

###### Theorem 3.4 (Preservation of System $\texttt{F}_{\texttt{<:QA}}$).

Suppose $\langle c,\kappa\rangle$ is a well-typed machine configuration. Then
if it steps to another configuration $\langle
c^{\prime},\kappa^{\prime}\rangle$, that configuration is also well typed.

Typing for System $\texttt{F}_{\texttt{<:QA}}$ $\Gamma\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}R$}\vdash s:T$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:T\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}R\vdash
x:T\end{array}}$ (A-var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,x:T_{1}\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}P$}\vdash
t:T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma~{}\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}\operatorname{\texttt{sync}}$}\vdash\lambda({x})_{P}.{t}:\\{{P}\\}~{}{{T_{1}}\to{T_{2}}}\end{array}}$
(A-abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,X~{}\texttt{<:}~{}S\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}P$}\vdash
t:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}\operatorname{\texttt{sync}}$}\vdash\Lambda({X}~{}\texttt{<:}~{}{S})_{P}.{t}:\\{{P}\\}~{}{\forall({X}~{}\texttt{<:}~{}{S}).{T}}\end{array}}$
(A-t-abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,Y~{}\texttt{<:}~{}Q\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}P$}\vdash
t:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}\operatorname{\texttt{sync}}$}\vdash\Lambda({Y}~{}\texttt{<:}~{}{Q})_{P}.{t}:\\{{P}\\}~{}{\forall({Y}~{}\texttt{<:}~{}{Q}).{T}}\end{array}}$
(A-q-abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}R$}\vdash t:\\{{\hbox{\pagecolor{light-
gray}$\displaystyle R$}}\\}~{}{{T_{1}}\to{T_{2}}}\quad\quad\Gamma\vdash
s:T_{1}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}R$}\vdash{t}({s}):T_{2}\end{array}}$ (A-app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}R$}\vdash t:\\{{\hbox{\pagecolor{light-
gray}$\displaystyle
R$}}\\}~{}{\forall({X}~{}\texttt{<:}~{}{S}).{T}}\quad\quad\Gamma\vdash
S^{\prime}~{}\texttt{<:}~{}S\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}R$}\vdash{t}[{S^{\prime}}]:T[X\mapsto
S^{\prime}]\end{array}}$ (A-t-app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}R$}\vdash t:\\{{\hbox{\pagecolor{light-
gray}$\displaystyle
R$}}\\}~{}{\forall({Y}~{}\texttt{<:}~{}{Q}).{T}}\quad\quad\Gamma\vdash
Q^{\prime}~{}\texttt{<:}~{}Q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\hbox{\pagecolor{light-
gray}$\displaystyle~{}|~{}R$}\vdash{t}\\{\\!\\!\\{{Q^{\prime}}\\}\\!\\!\\}:T[Y\mapsto
Q^{\prime}]\end{array}}$ (A-q-app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}R\vdash
s:T_{1}\quad\quad\Gamma\vdash
T_{1}~{}\texttt{<:}~{}T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}R\vdash
s:T_{2}\end{array}}$ (A-sub)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}R\vdash
s:T_{1}\quad\quad\Gamma\vdash
R~{}\texttt{<:}~{}Q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma~{}|~{}Q\vdash
s:T_{2}\end{array}}$ (A-sub-eff)

Figure 14. Typing rules for System $\texttt{F}_{\texttt{<:QA}}$

Note that progress and preservation guarantee meaningful safety properties
about System $\texttt{F}_{\texttt{<:QA}}$, namely that an asynchronous
function is never called above a synchronous function during evaluation, as
such a call would get stuck, by (reduce-app).

#### Observations

System $\texttt{F}_{\texttt{<:QA}}$ can be used to model function colouring
with other qualifiers as well; for example, we could model colours noexcept
and throws by assigning noexcept to $\bot$ and throws to $\top$. More
interestingly System $\texttt{F}_{\texttt{<:QA}}$ could be viewed as a simple
effect system; the synchronicity context $R$ can be seen as the effect of a
term! We discuss this curious connection between qualifiers and effects in
Section 7.3.

###  3.3. Tracking Capture

Finally, our design recipe can be remixed to construct a qualifier system to
qualify values based on what they capture. Some base values are meaningful and
should be tracked, and other values are forgettable.

#### Motivation

One application of such a system is the effects-as-capabilities discipline
(Dennis and Van Horn, 1966), which enables reasoning about which code can
perform side effects by simply tracking capabilities, special values that
grant the holder the ability to perform side effects; for example, the ability
to perform I/O, or the ability to throw an exception.

#### What to track?

Suppose for example we have a base capability named one_ring, which allows its
holder to produce arbitrary values. Such a precious value really ought to be
tracked and not forgotten, as in the hands of the wrong user, it can perform
dangerous side effects!

⬇

val one_ring : {tracked} [A] (Unit => A) = ???

However, it is not only one_ring itself that is dangerous. Actors that capture
one_ring can themselves cause dangerous side effects. For example:

⬇

def fifty_fifty(): Unit = {

val gauntlet = one_ring[InfinityGauntlet]()

gauntlet.snap()

} // one_ring is captured by fifty_fifty.

In general, values that capture meaningful values—capabilities—become
meaningful themselves, since they can perform side effects, so they should
also be tracked. Now, while it is clear that one_ring and fifty_fifty are both
dangerous, they are dangerous for different reasons: one_ring because it
intrinsically is and fifty_fifty because it captures one_ring.

#### Distinguishing Capabilities

In practical applications, we may wish to distinguish between different
effects, modelled by different capabilities. For example, we may wish to
reason about a more pedestrian side effect – printing – separately from the
great evil that one_ring can perform. It is reasonable to expect that we can
print in more contexts than we can use the one_ring.

⬇

val print : {tracked} String => Unit = ???

def hello_world() = print "Hello␣World!" // tracked as it captures print

def runCodeThatCanPrint(f: ??? () => Unit) = f()

runCodeThatCanPrint(hello_world) // OK

runCodeThatCanPrint(fifty_fifty) // Should be forbidden

In this example, function runCodeThatCanPrint only accepts thunks that print
as a side effect. What type annotation should we give to its argument f? In
particular, what qualifier should we use to fill in the blank? It should not
be tracked, as otherwise we could pass fifty_fifty to runCodeThatCanPrint – an
operation which should be disallowed. Instead we would like to fill that blank
with print; to denote that runCodeThatCanPrint can accept any thunk which is
no more dangerous than print itself. Figure 15 summarizes the different
variables in the above examples and the qualifiers we would like to assign to
their types.

Term |  Qualifier |  Reason
---|---|---
one_ring |  tracked |  As one_ring is a base capability.
print |  tracked |  As print is a base capability.
fifty_fifty |  one_ring |  As fifty_fifty is no more dangerous than one_ring.
hello_world |  print |  As hello_world is no more dangerous than print.
Figure 15. Qualifier assignments in Capture Tracking

As Odersky et al. (2021); Boruch-Gruszecki et al. (2021, 2023) show, such a capture tracking system could be used to guarantee desirable and important safety invariants. They model capture tracking using sets of variables, but a set is just a lattice join of the singletons in that set! For example, Boruch-Gruszecki et al. (2023) would give the following evil_monologue function the capture set annotation {fifty_fifty, print}, while we would give it the qualifier annotation {fifty_fifty | print}.

⬇

def evil_monologue(): Unit = {

print "I␣expect␣you␣to␣die,␣Mr.␣Bond."

fifty_fifty()

}

Using this insight, we can model capture tracking as an extension System
$\texttt{F}_{\texttt{<:QC}}$ of System $\texttt{F}_{\texttt{<:Q}}$.

$\begin{array}[t]{rll@{\hspace{4mm}}l}\\\ s,t&::=&\hfil\hskip
11.38109pt&\mbox{\bf{Terms}}\\\ &\ldots\\\
&|&{s}\\{\\!\\!\\{{Q}\\}\\!\\!\\}({t})\hfil\hskip 11.38109pt&\mbox{term
application}\\\\[6.0pt] S&::=&\hfil\hskip 11.38109pt&\mbox{\bf{Types}}\\\
&\ldots\\\ &|&({x}:{T_{1}})\to{T_{2}}\hfil\hskip 11.38109pt&\mbox{function
type}\\\\[6.0pt] P,Q,R&::=&\hfil\hskip 11.38109pt&\mbox{\bf{Qualifiers}}\\\
&\ldots&\hfil\hskip 11.38109pt&\mbox{as before, except:}\\\ &|&x\hfil\hskip
11.38109pt&\mbox{term variables}\\\
&|&\operatorname{\texttt{tracked}}~{}(\mbox{as }\top)\hfil\hskip
11.38109pt&\mbox{tracked values}\\\ \end{array}$

Evaluation: $s\;\longrightarrow\;t$

$\displaystyle\begin{array}[]{@{}c@{}}{(\lambda({x})_{P}.{t})}\\{\\!\\!\\{{\hbox{\pagecolor{light-
gray}$\displaystyle Q$}}\\}\\!\\!\\}({s})\;\longrightarrow\\\ t[x\mapsto_{\tt
type}Q][x\mapsto_{\tt term}s]\end{array}$ (C-beta-v)

Subqualification: $\Gamma\vdash Q~{}\texttt{<:}~{}R$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\\{{Q}\\}~{}{S}\in\Gamma\quad\quad\Gamma\vdash
Q~{}\texttt{<:}~{}R\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
x~{}\texttt{<:}~{}R\end{array}}$ (sq-tvar)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\\{{Q}\\}~{}{S}\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
x~{}\texttt{<:}~{}x\end{array}}$ (sq-refl-tvar)

Subtyping:  $\Gamma\vdash S_{1}~{}\texttt{<:}~{}S_{2}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
T_{1}~{}\texttt{<:}~{}T_{2}\quad\quad\Gamma,x:T_{1}\vdash
T_{3}~{}\texttt{<:}~{}T_{4}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash({x}:{T_{2}})\to{T_{3}}~{}\texttt{<:}~{}({x}:{T_{1}})\to{T_{4}}\end{array}}$
(C-sub-arrow)

Figure 16. Evaluation, Syntax, Subtyping for System
$\texttt{F}_{\texttt{<:QC}}$

#### Assigning Qualifiers

We attach a qualifier tracked to types, denoting which values we should keep
track of. The qualifier tracked induces a two-point lattice, where tracked is
at $\top$, and values that should not be tracked, or should be forgotten, are
qualified at $\bot$. Base capabilities will be given the tracked qualifier.

#### Syntax – Tracking Variables

Figure 16 defines the syntax of System $\texttt{F}_{\texttt{<:QC}}$. ’To
reflect the underlying term-variable-based nature of capture tracking, term
bindings in System $\texttt{F}_{\texttt{<:QC}}$ introduce both a term variable
in term position as well as a qualifier variable in qualifier position with
the same name as the term variable.

Term bindings now serve double duty introducing both term variables and
qualifier variables, so a term like the monomorphic identity function
$\lambda({x})_{\bot}.{x}$ would be given the type
$\\{{\bot}\\}~{}{({x}:{\\{{Q}\\}~{}{S}})\to{\\{{x}\\}~{}{S}}}$ to indicate
that it is not tracked but the result might be tracked depending on whether or
not its argument $x$ is tracked as well. This still induces a free lattice
structure generated over the two-point lattice that tracked induces, except in
this case, the free lattice includes both qualifier variables introduced by
qualifier binders in addition to qualifier variables introduced by term
binders as well. As term binders introduce both a term and qualifier variable,
term application in System $\texttt{F}_{\texttt{<:QC}}$ now requires a
qualifier argument to be substituted for that variable in qualifier position.
As such, term application in System $\texttt{F}_{\texttt{<:QC}}$ now has three
arguments ${s}\\{\\!\\!\\{{Q}\\}\\!\\!\\}({t})$ – a function $s$, a qualifier
$Q$, and an argument $t$; see Figure 16. In this sense, term abstractions in
System $\texttt{F}_{\texttt{<:QC}}$ can be viewed as a combination of a
qualifier abstraction $\Lambda[x<:Q]$ followed by a term abstraction
$\lambda(x:\\{{x}\\}~{}{T})$.

Typing for System $\texttt{F}_{\texttt{<:QC}}$ $\Gamma\vdash t:T$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\\{{Q}\\}~{}{S}\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
x:\\{{x}\\}~{}{S}\end{array}}$ (C-var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
s:({x}:{\\{{Q}\\}~{}{S}})\to{T}\quad\quad\Gamma\vdash
Q^{\prime}~{}\texttt{<:}~{}Q\\\ \Gamma\vdash
t:\\{{Q^{\prime}}\\}~{}{S}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{s}\\{\\!\\!\\{{Q^{\prime}}\\}\\!\\!\\}({t}):T[x\mapsto_{\tt
type}Q^{\prime}]\end{array}}$ (C-app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,x:T_{1}\vdash
t:T_{2}\quad\quad\hbox{\pagecolor{light-
gray}$\displaystyle\Gamma\vdash\vee_{y\in\operatorname{\texttt{fv}}(t)-x}~{}y~{}\texttt{<:}~{}P$}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\lambda({x})_{P}.{t}:\\{{P}\\}~{}{({x}:{T_{1}})\to{T_{2}}}\end{array}}$
(C-abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,X~{}\texttt{<:}~{}S\vdash
t:T\quad\quad\hbox{\pagecolor{light-
gray}$\displaystyle\Gamma\vdash\vee_{y\in\operatorname{\texttt{fv}}(t)}~{}y~{}\texttt{<:}~{}P$}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\Lambda({X}~{}\texttt{<:}~{}{S})_{P}.{t}:\\{{P}\\}~{}{\forall({X}~{}\texttt{<:}~{}{S}).{T}}\end{array}}$
(C-t-abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,X~{}\texttt{<:}~{}S\vdash
t:T\quad\quad\hbox{\pagecolor{light-
gray}$\displaystyle\Gamma\vdash\vee_{y\in\operatorname{\texttt{fv}}(t)}~{}y~{}\texttt{<:}~{}P$}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\Lambda({Y}~{}\texttt{<:}~{}{Q})_{P}.{t}:\\{{P}\\}~{}{\forall({Y}~{}\texttt{<:}~{}{Q}).{T}}\end{array}}$
(C-q-abs)

Figure 17. Typing rules for System $\texttt{F}_{\texttt{<:QC}}$

#### Subqualification

One essential change is that we need to adjust subqualification to account for
qualifier variables bound by term binders in addition to qualifier variables
bound by qualifier binders. These changes are the addition of two new rules,
(sq-refl-tvar) and (sq-tvar). Rule (sq-refl-tvar) accounts for reflexivity in
System $\texttt{F}_{\texttt{<:QC}}$’s adjusted subqualification judgment. (sq-
tvar) accounts for subqualification for qualifier variables bound by term
binders, and formalizes this notion of less dangerous we discussed
earlier—that fifty_fifty can be used in a context that allows the use of
one_ring, and that hello_world can be used in a context that allows the use of
print. Interestingly, it is just a close duplicate of the existing
subqualification rule for qualifier variables, (sq-var)!

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\hbox{\pagecolor{qualifier-blue-
bg}\color[rgb]{0.17578125,0.37109375,0.52734375}\definecolor[named]{pgfstrokecolor}{rgb}{0.17578125,0.37109375,0.52734375}{\tt
fifty\\_fifty}}:\hbox{\pagecolor{qualifier-blue-
bg}\color[rgb]{0.17578125,0.37109375,0.52734375}\definecolor[named]{pgfstrokecolor}{rgb}{0.17578125,0.37109375,0.52734375}{\tt
one\\_ring}}~{}{\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color<EMAIL_ADDRESS>Unit=>Unit}\in\Gamma\quad\quad\Gamma\vdash\hbox{\pagecolor{qualifier-blue-
bg}\color[rgb]{0.17578125,0.37109375,0.52734375}\definecolor[named]{pgfstrokecolor}{rgb}{0.17578125,0.37109375,0.52734375}{\tt
one\\_ring}}~{}\texttt{<:}~{}\hbox{\pagecolor{qualifier-blue-
bg}\color[rgb]{0.17578125,0.37109375,0.52734375}\definecolor[named]{pgfstrokecolor}{rgb}{0.17578125,0.37109375,0.52734375}{\tt
one\\_ring}}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\hbox{\pagecolor{qualifier-
blue-
bg}\color[rgb]{0.17578125,0.37109375,0.52734375}\definecolor[named]{pgfstrokecolor}{rgb}{0.17578125,0.37109375,0.52734375}{\tt
fifty\\_fifty}}~{}\texttt{<:}~{}\hbox{\pagecolor{qualifier-blue-
bg}\color[rgb]{0.17578125,0.37109375,0.52734375}\definecolor[named]{pgfstrokecolor}{rgb}{0.17578125,0.37109375,0.52734375}{\tt
one\\_ring}}\end{array}}$

#### Subtyping

As function binders introduce a qualifier variable, so do function types as
well; for example, $x$ in $({x}:{\\{{Q}\\}~{}{S}})\to{\\{{x}\\}~{}{S}}$.
Subtyping needs to account for this bound qualifier variable; see (C-sub-
arrow).

#### Typing

Values are now qualified with the free variables that they close over (i.e.,
that they capture). To ensure this is faithfully reflected in the value
itself, we check that the tag on the value super-qualifies the free variables
that value captures. This is reflected in the modified typing rules for typing
abstractions: (C-abs), (C-t-abs), and (C-q-abs). The only other apparent
changes are in the rules for term application typing and variable typing.
While those rules look different, they reflect how term abstractions are a
combination of qualifier and term abstractions, and in that setting are no
different than the standard rules for typing term variables, term application,
and qualifier application! These changes to the typing rules are reflected in
Figure 17.

#### Soundness

Again, we can prove the standard soundness theorems for System
$\texttt{F}_{\texttt{<:QC}}$, using similar techniques as Lee et al. (2023).

###### Theorem 3.5 (Preservation for System $\texttt{F}_{\texttt{<:QC}}$).

Suppose $\Gamma\vdash s:T$, and $s\;\longrightarrow\;t$. Then $\Gamma\vdash
t:T$ as well.

###### Theorem 3.6 (Progress for System $\texttt{F}_{\texttt{<:QC}}$).

Suppose $\varnothing\vdash s:T$. Either $s$ is a value, or
$s\;\longrightarrow\;t$ for some term $t$.

In addition, we recover a prediction lemma (Odersky et al., 2021, 2022;
Boruch-Gruszecki et al., 2021) relating how the free variables of values
relate to the qualifier annotated on their types; in essence, that the
qualifier given on the type contains the free variables present in the value
v.

###### Lemma 3.7 (Capture Prediction for System $\texttt{F}_{\texttt{<:QC}}$).

Let $\Gamma$ be an environment and $v$ be a value such that $\Gamma\vdash
v:\\{{Q}\\}~{}{S}$. Then
$\Gamma\vdash\left\\{\bigvee_{y\in\operatorname{\texttt{fv}}(v)}y\right\\}~{}\texttt{<:}~{}Q$.

##  4\. Mechanization

The mechanization of System $\texttt{F}_{\texttt{<:Q}}$ (from Section 2.3),
its derived calculi, System $\texttt{F}_{\texttt{<:QM}}$, System
$\texttt{F}_{\texttt{<:QA}}$, and System $\texttt{F}_{\texttt{<:QC}}$, (from
Section 3), and extended System $\texttt{F}_{\texttt{<:Q}}$ (from Section
2.6), is derived from the mechanization of System $\texttt{F}_{\texttt{<:}}$
by Aydemir et al. (2008), with some inspiration taken from the mechanization
of Lee et al. (2023) and Lee and Lhoták (2023). All lemmas and theorems stated
in this paper regarding these calculi have been formally mechanized, though
our proofs relating the subqualification structure to free lattices are only
proven in text, as we have found Coq’s tooling for universal algebra lacking.

##  5\. Type polymorphism and Qualifier polymorphism

We chose to model polymorphism separately for qualifiers and simple types. We
introduced a third binder, qualifier abstraction, for enabling polymorphism
over type qualifiers, orthogonal to simple type polymorphism. An alternate
approach one could take to design a language which needs to model polymorphism
over type qualifiers is to have type variables range over qualified types,
that is, types like mutable Ref[Int] as well as const Ref[Int]. This approach
can been seen in systems like Tschantz and Ernst (2005); Zibin et al. (2010);
Lee and Lhoták (2023). However, it also comes with its difficulties: how do we
formally interpret repeated applications of type qualifiers? For example, with
a generic inplace_map which maps a function over a reference cell?

⬇

case class Ref[X](var elem: X)

// Is this well formed?

def inplace_map[X](r: mutable Ref[X], f: const X => X): Unit = {

r.elem = f(r.elem);

}

For example, what if inplace_map is applied on a Ref[const Ref[Int]]? Then
inplace_map would expect a function f with type (const (const Ref[Int])) =>
const Ref[Int]. While our intuition would tell us that const (const Ref[Int])
is really just a const Ref[Int], discharging this equivalence in a proof is
not so easy. Many systems, like Zibin et al. (2007)’s and Tschantz and Ernst
(2005)’s sidestep this issue by explicitly preventing type variables from
being further qualified, but this approach prevents functions like inplace_map
from being expressed at all. Another approach, taken by Lee and Lhoták (2023),
is to show that these equivalences can be discharged through subtyping rules
which normalize equivalent types. However, their approach led to complexities
in their proof of soundness and it is unclear if their system admits
algorithmic subtyping rules.

Our proposed approach, while verbose, avoids all these complexities by
explicitly keeping simple type polymorphism separate from type qualifier
polymorphism. We would write inplace_map as:

⬇

case class Ref[Q, X](var elem: Q X)

def inplace_map[Q, X](r: mutable Ref[{Q} X], f: const X => Q X): Unit = {

r.elem = f(r.elem);

}

Moreover, we can desugar qualified type polymorphism into a combination of
simple type polymorphism and type qualifier polymorphism. We can treat a
qualified type binder in surface syntax as a pair of simple type and type
qualifier binders, and have qualified type variables play double duty as
simple type variables and type qualifier variables, as seen in qualifier
systems like Wei et al. (2023)’s. So our original version of inplace_map could
desugar as follows:

⬇

def inplace_map[X](r: mutable Ref[X], f: const X => X): Unit = {

r.elem = f(r.elem);

} // original

def inplace_map[Xq, Xs](r: mutable[{Xq} Xs], f: const Xs => Xs): Unit = {

r.elem = f(r.elem);

} // desugared ==> X splits into Xq and Xs

One problem remains for the language designer however: how do type qualifiers
interact with qualified type variables? In our above example we chose to have
the new qualifier annotation const X strip away any existing type qualifier on
X; this is the approach that Papi et al. (2008)’s Checker Framework take.
Alternatively, we could instead merge the qualifiers together:

⬇

def inplace_map[Xq, Xs](r: mutable[{Xq} Xs], f: {const | Xq} Xs => Xs): Unit =

{

r.elem = f(r.elem);

} // desugared ==> X splits into Xq and Xs

##  6\. Revisiting Qualifier Systems

Free lattices have been known by mathematicians since Whitman (1941)’s time as
the proper algebraic structure for modelling lattice inequalities involving
formulas with variables—word problems—over arbitrary lattices. In this light
it is somewhat surprising that existing qualifier systems have not taken
advantage of that structure explicitly, especially so given that is folklore
knowledge in the literature that intersection and union types make the
subtyping lattice a free lattice as well as Dolan (2016) observed. Here, we
revisit some existing qualifier systems to examine how their qualifier
structure compares to the structure we present with the free lattice of
qualifiers.

#### A Theory of Type Qualifiers

Foster et al. (1999)’s original work introduced the notion of type qualifiers,
and gave a system for ML-style let polymorphism using a variant of Odersky et
al. (1999)’s HM(X) constraint-based type inference. Qualifier-polymorphic
types in Foster’s polymorphic qualifier system are a type scheme
$\forall\overline{Y}/C.T$ for some vector of qualifier variables
$\overline{Y}$ used in qualified type $T$ modulo qualifier ordering
constraints in $C$, such as $Y_{1}~{}\texttt{<:}~{}Y_{2}$. However, in their
system, constraints cannot involve formulas with qualifier variables
$X~{}\texttt{<:}~{}Y_{1}\wedge Y_{2}$ is an invalid constraint, nor are
constraints expressible in their source syntax for qualifier-polymorphic
function terms.

#### Qualifiers for Tracking Capture and Reachability

Our subqualification system was inspired by the subcapturing system pioneered
by Boruch-Gruszecki et al. (2023) for use in their capability tracking system
for Scala. They model sets of free variables coupled with operations for
merging sets together. Sets of variables are exactly joins of variables – the
set $\\{a,b,c\\}$ can be viewed as the lattice formula $a\vee b\vee c$, and
their set-merge substitution operator
$\\{a,b,c\\}[a\mapsto\\{d,e\\}]=\\{d,e,b,c\\}$, is just substitution for free
lattice formulas – $(a\vee b\vee c)[a\mapsto(d\vee e)]=(d\vee e)\vee b\vee c$.
With this translation in mind we can see that they model a free
(join)-semilattice, and that their subcapturing rules involving variables in
sets are just translating what the lattice join would be into a set framework.

Independently, Wei et al. (2023) recently developed a qualifier system for
tracking reachability using variable sets as well. Like Boruch-Gruszecki et
al. (2023), their subqualification system models a free join-semilattice, with
one additional wrinkle. They model a notion of set overlap respecting their
subcapturing system as well as a notion of freshness in their framework to
ensure that the set of values reachable from a function are disjoint, or
fresh, from the set of values reachable from that function’s argument. While
overlap exists only at the metatheoretic level and does not exist in the
qualifier annotations it can be seen that their notion of overlap is exactly
the what the lattice meet of their set-qualifiers would be when interpreted as
lattice terms. Additionally, while freshness unfortunately does not fit in the
framework of a free lattice, we conjecture that freshness can be modelled in a
setting where lattices are extended with complementation as well, such as in
free complemented distributive lattices.

#### Boolean Formulas as Qualifiers

Madsen and van de Pol (2021) recently investigated modelling nullability as a
type qualifier. Types in their system comprise a scheme of type variables
$\overline{\alpha}$ and Boolean variables $\overline{\beta}$ over a pair of
simple type $S$ and Boolean formula $(S,\phi)$, where values of a qualified
type $(S,\phi)$ are nullable if and only if $\phi$ evaluates to
true.111Technically they model a triple $(S,\phi,\gamma)$ where $\gamma$ is
another Boolean formula which evaluates to true if values of type
$(S,\phi,\gamma)$ are non-nullable. Boolean formulas form a Boolean algebra,
and Boolean algebras are just complemented distributive lattices, so Boolean
formulas over a set of variables $\overline{\beta}$ are just free complemented
distributive lattices generated over variables in $\overline{\beta}$. In this
sense, we can view Madsen and van de Pol (2021) as a ML-polymorphism style
extension of Foster et al. (1999)’s original work which solves Foster’s
original problem of encoding qualifier constraints: one can just encode them
using Boolean formulas in Madsen and van de Pol (2021)’s system.

Unfortunately they do not model subtyping over their qualified types
$(S,\phi)$; it would be sensible to say
$(S,\phi)~{}\texttt{<:}~{}(S,\phi^{\prime})$ if $\phi\implies\phi^{\prime}$.
They conjecture that such a subtyping system would be sound however. While we
cannot answer this conjecture definitively, as we only model free lattices,
not free complemented distributive lattice systems, it would be interesting
future work to extend our framework and theirs to see if a system modelling
free complemented distributive lattice systems with subqualification is sound.

#### Reference Immutability for C# (Gordon et al., 2012)

Of existing qualifier systems, the the polymorphism structure of Gordon et al.
(2012) is closest to System $\texttt{F}_{\texttt{<:Q}}$. Polymorphism is
possible over both mutability qualifiers and simple types in Gordon’s system,
but must be done separately, as in System $\texttt{F}_{\texttt{<:Q}}$. The
inplace_map function that we discussed earlier would be expressed with both a
simple type variable as well as with a qualifier variable:

⬇

def inplace_map[Q, X](r: mutable Ref[{Q} X], f: readonly X => {Q} X): Unit

Gordon’s system also allows for mutability qualifiers to be merged using an
operator ~>. For example, a polymorphic read function read could be written as
the following in Gordon’s system:

⬇

def read[QR, QX, X](r: {QR} Ref[{QX} X]): {QR ~> QX} X = r.f

Now, ~> acts as a restricted lattice join. Given two concrete mutability
qualifiers C and D, C ~> D will reduce to the lattice join of $C$ and $D$.
However, the only allowable judgment in Gordon’s system for ~> when qualifier
variables are present, say C ~> Y, is that it can be widened to readonly.

#### Reference Immutability for DOT (Dort and Lhoták, 2020)

roDOT extends the calculus of Dependent Object Types (Amin et al., 2016) with
support for reference immutability. In their system, immutability constraints
are expressed through a type member field $x.M$ of each object, where $x$ is
mutable if and only if $M\leq\bot$, and $x$ is read-only if and only if
$M\geq\top$. As $M$ is just a Scala type member, $M$ can consist of anything a
Scala type could consist of, but typically it consists of type meets and type
joins of $\top$, $\bot$, type variables $Y$, and the mutability members $y.M$
of other Scala objects $y$.

While this may seem odd, we can view $M$ as a type qualifier member field of
its containing object $x$; the meets and joins in roDOT’s $M$’s subtyping
lattice correspond to meets and joins in System $\texttt{F}_{\texttt{<:Q}}$’s
subqualification lattice. In this sense we can view type polymorphism in roDOT
as a combination of polymorphism over simple types and type qualifiers in
System $\texttt{F}_{\texttt{<:Q}}$. A type $T$ in roDOT breaks down into a
pair of a simple type $T\setminus M$ – $T$ without its mutability member $M$
and $M$ itself. In this sense Dort and Lhoták (2020) provide a different
method to encode subqualification; they encode it in type members $M$ and
reuse the subtyping lattice to encode the free lattice structure needed to
deal with qualifier polymorphism and qualifier variables.

##  7\. Related Work

###  7.1. Languages with Type Qualifier Systems

#### Rust

The Rust community is currently investigating approaches (Wuyts et al., 2022)
for adding qualifiers to Rust. Their current proposal is to generalize the
notion of qualified types from being a pair of one qualifier and base type to
be a tuple of qualifiers coupled to a base type. Qualifier abstractions are
keyed with the kind of qualifier (const, async, etc, …) they abstract over.

This is easy to see sound using similar ideas to our proof of simplified
System $\texttt{F}_{\texttt{<:Q}}$, and avoids the complications around
subqualification that free lattices over arbitrary lattices pose. However this
proposal has proven controversial in the Rust community due the additional
syntactic complexity it imposes.

#### OCaml

The OCaml community (Slater, 2023b, a) is investigating adding modes to types
for tracking, in addition to value shapes, properties like uniqueness,
locality, and ownership, amongst others; these modes are essentially type
qualifiers. However, modal polymorphism still remains an open problem in
OCaml.

#### Pony

Pony’s reference capabilities (Clebsch et al., 2015) are essentially type
qualifiers on base types that qualify how values may be shared or used. Pony
has qualifiers for various forms of uniquness, linearity, and ownership
properties. While Pony has bounded polymorphism over qualified types, Pony
does not allow type variables to be requalified, nor does it have polymorphism
over qualifiers.

###  7.2. Implementing Type Qualifiers

The Checker Framework by Papi et al. (2008) is an extensible framework for
adding user-defined type qualifiers to Java’s type system. The Checker
Framework in general allows for qualifying type variables with types, but in
their system there is no relationship between a type variable X and a
qualified type variable Q X. Re-qualifying a type variable strips any existing
conflicting qualifier from that type variable and what it is instantiated
with.

###  7.3. Effect Systems

Effect systems are closely related to type qualifiers. Traditionally, effect
annotations are used to describe properties of computation, whereas type
qualifiers are used to describe properties of data. In the presence of first-
class functions, this distinction is often blurred; for example, modern C++
refers to noexcept as a type qualifier on function types (Maurer, 2015),
whereas traditionally it would be viewed as an effect annotation. In contrast
to type qualifiers, both effect polymorphism (Lucassen and Gifford, 1988) and
the lattice structure of effects (Rytz et al., 2012) are well-studied.
However, the interaction of effect polymorphism with subtyping and sub-
effecting remains understudied.

Many effect systems use row polymorphism to handle polymorphic effect
variables with a restricted form of sub-effecting by subsets (Leijen, 2014).
As for Rytz et al. (2012), they present a lightweight framework with no effect
variables. Formal systems studying sub-effecting respecting effect bounds on
effect variables remain rare, despite Java’s exception system being just that
(Gosling et al., 2014, Section 8.4.8.3). Curiously, the two extant formal
effect systems with these features share much in common with well-known
qualifier systems. For example, Leijen and Tate (2010)’s sub-effecting system
can be viewed as a variant of Foster et al. (1999)’s lattice-based
subqualification system with HM(X)-style polymorphism. More interestingly,
Gariano et al. (2019)’s novel Indirect-Call$\varepsilon$ rule, Wei et al.
(2023)’s reachability rule, and Boruch-Gruszecki et al. (2023)’s subcapturing
rule all model a free join-semilattice (of effects). In light of all these
similarities, and of Lutze et al. (2023)’s recent work modelling effect
systems with Boolean formulas, we conjecture that a system modelling free
distributive complemented lattices could be used to present an unifying
treatment of both effects and qualifiers in the presence of subtyping,
subeffecting, and subqualification.

##  8\. Conclusion

In this paper, we presented a recipe for modelling higher-rank polymorphism,
subtyping, and subqualification in systems with type qualifiers by using the
free lattice generated from an underlying qualifier lattice. We show how a
base calculus like System $\texttt{F}_{\texttt{<:}}$ can be extended using
this structure by constructing such an extension System
$\texttt{F}_{\texttt{<:Q}}$, and we show how the recipe can be applied to
model three problems where type qualifiers are naturally suited—reference
immutability, function colouring, and capture tracking. We then re-examine
existing qualifier systems to look at how free lattices of qualifiers show up,
even indirectly or in restricted form. We hope that this work advances our
understanding of the structure of polymorphism over type qualifiers.

###### Acknowledgements.

We thank Brad Lushman, John Boyland, and Guannan Wei for their useful feedback
in reading over early drafts of this work. We also thank Ross Willard for his
useful insights into free lattices. This work was partially supported by the
Natural Sciences and Engineering Research Council of Canada and by an Ontario
Graduate Scholarship.

## References

  * (1)
  * Amin et al. (2016) Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016\.  The essence of dependent object types.  _A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday_ (2016), 249–272.
  * Aydemir et al. (2008) Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. 2008\.  Engineering Formal Metatheory. In _Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Francisco, California, USA) _(POPL ’08)_. Association for Computing Machinery, New York, NY, USA, 3–15.  https://doi.org/10.1145/1328438.1328443
  * Boruch-Gruszecki et al. (2021) Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, Ondřej Lhoták, and Martin Odersky. 2021.  Tracking Captured Variables in Types.  arXiv:2105.11896 [cs.PL]
  * Boruch-Gruszecki et al. (2023) Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondřej Lhoták, and Jonathan Brachthäuser. 2023.  Capturing Types.  _ACM Trans. Program. Lang. Syst._ (sep 2023).  https://doi.org/10.1145/3618003 Just Accepted.
  * Bright et al. (2020) Walter Bright, Andrei Alexandrescu, and Michael Parker. 2020\.  Origins of the D Programming Language.  _Proc. ACM Program. Lang._ 4, HOPL, Article 73 (jun 2020), 38 pages.  https://doi.org/10.1145/3386323
  * Clebsch et al. (2015) Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. 2015.  Deny Capabilities for Safe, Fast Actors. In _Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control_ (Pittsburgh, PA, USA) _(AGERE! 2015)_. Association for Computing Machinery, New York, NY, USA, 1–12.  https://doi.org/10.1145/2824815.2824816
  * Dennis and Van Horn (1966) Jack B. Dennis and Earl C. Van Horn. 1966.  Programming Semantics for Multiprogrammed Computations.  _Commun. ACM_ 9, 3 (mar 1966), 143–155.  https://doi.org/10.1145/365230.365252
  * Dolan (2016) Stephen Dolan. 2016\.  _Algebraic subtyping_.  Ph. D. Dissertation.
  * Dort and Lhoták (2020) Vlastimil Dort and Ondřej Lhoták. 2020.  Reference Mutability for DOT. In _34th European Conference on Object-Oriented Programming (ECOOP 2020)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166)_ , Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 18:1–18:28.  https://doi.org/10.4230/LIPIcs.ECOOP.2020.18
  * Felleisen and Friedman (1987) Mattias Felleisen and D. P. Friedman. 1987.  A Calculus for Assignments in Higher-Order Languages. In _Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages_ (Munich, West Germany) _(POPL ’87)_. Association for Computing Machinery, New York, NY, USA, 314.  https://doi.org/10.1145/41625.41654
  * Foster et al. (1999) Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. 1999\.  A Theory of Type Qualifiers. In _Proceedings of the ACM SIGPLAN 1999 Conference on Programming Language Design and Implementation_ (Atlanta, Georgia, USA) _(PLDI ’99)_. Association for Computing Machinery, New York, NY, USA, 192–203.  https://doi.org/10.1145/301618.301665
  * Gariano et al. (2019) Isaac Oscar Gariano, James Noble, and Marco Servetto. 2019\.  Call$\varepsilon$: an effect system for method calls. In _Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2019, Athens, Greece, October 23-24, 2019_ , Hidehiko Masuhara and Tomas Petricek (Eds.). ACM, 32–45.  https://doi.org/10.1145/3359591.3359731
  * Gordon et al. (2012) Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. 2012\.  Uniqueness and Reference Immutability for Safe Parallelism. In _Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications_ (Tucson, Arizona, USA) _(OOPSLA ’12)_. Association for Computing Machinery, New York, NY, USA, 21–40.  https://doi.org/10.1145/2384616.2384619
  * Gosling et al. (2014) James Gosling, Bill Joy, Guy L. Steele, Gilad Bracha, and Alex Buckley. 2014.  _The Java Language Specification, Java SE 8 Edition_ (1st ed.).  Addison-Wesley Professional.
  * Huang et al. (2012) Wei Huang, Ana Milanova, Werner Dietl, and Michael D. Ernst. 2012\.  ReIm and ReImInfer: Checking and Inference of Reference Immutability and Method Purity. In _Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications_ (Tucson, Arizona, USA) _(OOPSLA ’12)_. Association for Computing Machinery, New York, NY, USA, 879–896.  https://doi.org/10.1145/2384616.2384680
  * Karger and Herbert (1984) Paul A. Karger and Andrew J. Herbert. 1984.  An Augmented Capability Architecture to Support Lattice Security and Traceability of Access. In _1984 IEEE Symposium on Security and Privacy_. 2–2.  https://doi.org/10.1109/SP.1984.10001
  * Lee and Lhoták (2023) Edward Lee and Ondřej Lhoták. 2023.  Simple Reference Immutability for System $\text{F}_{\text{<:}}$.  _Proc. ACM Program. Lang._ 7, OOPSLA2, Article 252, 25 pages.  https://doi.org/10.1145/3622828
  * Lee et al. (2023) Edward Lee, Kavin Satheeskumar, and Ondřej Lhoták. 2023\.  Dependency-Free Capture Tracking. In _Proceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs_. Seattle, WA.  https://doi.org/10.1145/3605156.3606454
  * Leijen (2014) Daan Leijen. 2014\.  Koka: Programming with Row Polymorphic Effect Types.  _Electronic Proceedings in Theoretical Computer Science_ 153 (jun 2014), 100–126.  https://doi.org/10.4204/eptcs.153.8
  * Leijen and Tate (2010) Daan Leijen and Ross Tate. 2010.  _Convenient Explicit Effects using Type Inference with Subeffects_.  Technical Report MSR-TR-2010-80.  https://www.microsoft.com/en-us/research/publication/convenient-explicit-effects-using-type-inference-with-subeffects/
  * Lucassen and Gifford (1988) J. M. Lucassen and D. K. Gifford. 1988.  Polymorphic Effect Systems. In _Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Diego, California, USA) _(POPL ’88)_. Association for Computing Machinery, New York, NY, USA, 47–57.  https://doi.org/10.1145/73560.73564
  * Lutze et al. (2023) Matthew Lutze, Magnus Madsen, Philipp Schuster, and Jonathan Immanuel Brachthäuser. 2023\.  With or Without You: Programming with Effect Exclusion.  _Proc. ACM Program. Lang._ 7, ICFP, Article 204 (aug 2023), 28 pages.  https://doi.org/10.1145/3607846
  * Madsen and van de Pol (2021) Magnus Madsen and Jaco van de Pol. 2021.  Relational Nullable Types with Boolean Unification.  _Proc. ACM Program. Lang._ 5, OOPSLA, Article 110 (oct 2021), 28 pages.  https://doi.org/10.1145/3485487
  * Maurer (2015) Jens Maurer. 2015\.  P0012R1: Make exception specifications be part of the type system, version 5.  https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2015/p0012r1.html
  * Nystrom (2015) Bob Nystrom. 2015\.  What Color is Your Function?  https://journal.stuffwithstuff.com/2015/02/01/what-color-is-your-function/
  * Odersky et al. (2021) Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondřej Lhoták. 2021\.  Safer Exceptions for Scala. In _Proceedings of the 12th ACM SIGPLAN International Symposium on Scala_ (Chicago, IL, USA) _(SCALA 2021)_. Association for Computing Machinery, New York, NY, USA, 1–11.  https://doi.org/10.1145/3486610.3486893
  * Odersky et al. (2022) Martin Odersky, Aleksander Boruch-Gruszecki, Edward Lee, Jonathan Brachthäuser, and Ondřej Lhoták. 2022\.  Scoped Capabilities for Polymorphic Effects.  arXiv:2207.03402 [cs.PL]
  * Odersky et al. (1999) Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999\.  Type Inference with Constrained Types.  _Theory Pract. Object Syst._ 5, 1 (1999), 35–55.
  * Papi et al. (2008) Matthew M. Papi, Mahmood Ali, Telmo Luis Correa, Jeff H. Perkins, and Michael D. Ernst. 2008.  Practical Pluggable Types for Java. In _Proceedings of the 2008 International Symposium on Software Testing and Analysis_ (Seattle, WA, USA) _(ISSTA ’08)_. Association for Computing Machinery, New York, NY, USA, 201–212.  https://doi.org/10.1145/1390630.1390656
  * Petricek et al. (2014) Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2014\.  Coeffects: A Calculus of Context-Dependent Computation. In _Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming_ (Gothenburg, Sweden) _(ICFP ’14)_. Association for Computing Machinery, New York, NY, USA, 123–135.  https://doi.org/10.1145/2628136.2628160
  * Rytz et al. (2012) Lukas Rytz, Martin Odersky, and Philipp Haller. 2012\.  Lightweight Polymorphic Effects. In _ECOOP 2012 – Object-Oriented Programming_ , James Noble (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 258–282.
  * Slater (2023a) Max Slater. 2023a.  Oxidizing OCaml: Locality.  https://blog.janestreet.com/oxidizing-ocaml-locality/
  * Slater (2023b) Max Slater. 2023b.  Oxidizing OCaml: Rust-Style Ownership.  https://blog.janestreet.com/oxidizing-ocaml-ownership/
  * Stroustrup (2007) Bjarne Stroustrup. 2007\.  _The C++ programming language - special edition (3. ed.)_.  Addison-Wesley.
  * Tschantz and Ernst (2005) Matthew S. Tschantz and Michael D. Ernst. 2005.  Javari: adding reference immutability to Java. In _Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA_ , Ralph E. Johnson and Richard P. Gabriel (Eds.). ACM, 211–230.  https://doi.org/10.1145/1094811.1094828
  * Wei et al. (2023) Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, and Tiark Rompf. 2023.  Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs.  arXiv:2307.13844 [cs.PL]
  * Whitman (1941) Philip M. Whitman. 1941\.  Free Lattices.  _Annals of Mathematics_ 42, 1 (1941), 325–330.  http://www.jstor.org/stable/1969001
  * Wuyts et al. (2022) Yoshua Wuyts, Oli Scherer, and Niko Matsakis. 2022\.  Announcing the keyword generics initiative: Inside rust blog.  https://blog.rust-lang.org/inside-rust/2022/07/27/keyword-generics.html
  * Zibin et al. (2007) Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kiezun, and Michael D. Ernst. 2007\.  Object and Reference Immutability Using Java Generics. In _Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering_ (Dubrovnik, Croatia) _(ESEC-FSE ’07)_. Association for Computing Machinery, New York, NY, USA, 75–84.  https://doi.org/10.1145/1287624.1287637
  * Zibin et al. (2010) Yoav Zibin, Alex Potanin, Paley Li, Mahmood Ali, and Michael D. Ernst. 2010.  Ownership and immutability in generic Java. In _OOPSLA 2010, Object-Oriented Programming Systems, Languages, and Applications_. Revo, NV, USA, 598–617.