31.1 Intuitions

---

31.1 Intuitions

The interaction of subtyping and bounded quantification with type operators raises several design issues in the formulation of the combined system. We discuss these briefly before proceeding to the definition of the system.

The first question is whether, in the presence of subtyping, type operators like λX::K₁.T₂ should be generalized to bounded type operators of the form λX<:T₁ .T₂. We choose simplicity over regularity in this chapter, defining a system with bounded quantification and unbounded type operators. ^[1]

 
Figure 31-1: Higher-Order Bounded Quantification ()

The next issue is how to extend the subtype relation to include type operators. There are several alternatives. The simplest one, which we choose here, is to lift the subtype relation on proper types pointwise to type operators. For abstractions, we say that λX.S is a subtype of λX.T whenever applying both to any argument U yields types that are in the subtype relation. For example, λX.Top→X is a subtype of λX.X→Top because Top→U is a subtype of U→Top for every U. Equivalently, we can say that λX.S is a subtype of λX.T if S is a subtype of T when we hold X abstract, making no assumptions about its subtypes and supertypes. The latter view leads directly to the following rule:

Conversely, if F and G are type operators with F <: G, then F U <: G U.

Note that this rule applies only when F and G are applied to the same argument U—knowing that F is pointwise a subtype of G tells us nothing about their behavior when applied to different arguments. (Some more complex variants of that do consider this case are mentioned in §31.4.)

One additional rule arises from the intended meaning of the type equivalence relation. If S = T, then S and T have the same members. But types that have the same members are surely subtypes of one another. This leads to another subtyping rule, which includes definitional equivalence as a base case.

Having lifted subtyping from kind * to kind *⇒*, we can repeat the process for more complex kinds. For example, if P and Q are type operators of kind *⇒*⇒*, then we say P <: Q if, for each U, the application P U is a subtype of Q U in kind *⇒*.

A useful side effect of this definition is that the subtype relations for higher kinds all have maximal elements. If we let Top[*] = Top and define(maximal elements of higher kinds)

then a simple induction shows that Г ⊢ S <: Top[K] (whenever S has kind K). We exploit this effect in the rules in the following section.

The step from ordinary bounded quantifiers to higher-order bounded quantifiers is a straightforward one. inherits from F_<:bounded quantifiers of the form "X<:T₁.T₂. Generalizing to higher-order (i.e., to quantification over type operators) requires no change to this syntax: we just observe that T₁ here may be any type expression, including a type operator. The unbounded higher-order quantifiers that we inherit from F_ω can be treated as abbreviations for bounded quantifiers with maximal bounds—i.e., we regard "X::K₁.T₂ as an abbreviation for "X<:Top[K₁].T₂.

Lastly, inherits from F_<: the issue of whether to use the more tractable kernel variant or the more powerful full variant of the rule S-All. We choose the kernel variant here; the full variant also makes semantic sense, but its metatheoretic properties (even those that one would expect should hold, by analogy with full F_<:) have not yet been established.

^[1]The system studied in this chapter is pure (Figure 31-1). The associated implementation is fomsub (the fullfomsub implementation includes various extensions such as existentials).

---