16.1 Algorithmic Subtyping

---

16.1 Algorithmic Subtyping

A crucial element of any implementation of a language with subtyping is an algorithm for checking whether one type is a subtype of another. This subtype checker will be called by the typechecker when, for example, it encounters an application t₁ t₂ where t₁ has type T→U and t₂ has type S. Its function is to decide whether the statement S <: T is derivable from the subtyping rules in Figures 15-1 and 15-3. It accomplishes this by checking whether (S, T) belongs to another relation, written ("S is algorithmically a subtype of T"), which is defined in such a way that membership can be decided simply by following the structure of the types, and which contains the same pairs of types as the ordinary subtype relation. The significant difference between the declarative and algorithmic relations is that the algorithmic relation drops the S-TRANS and S-REFL rules.

To begin with, we need to reorganize the declarative system a little. As we saw on page 184, we need to use transitivity to "paste together" subtyping derivations for records involving combinations of depth, width, and permutation subtyping. Before we can drop S-TRANS, we must first add a rule that bundles depth, width, and permutation subtyping into one:

16.1.1 Lemma

If S <: T is derivable from the subtyping rules including S-RCDDEPTH, S-RCD-WIDTH, and S-RCD-PERM (but not S-RCD), then it can also be derived using S-RCD (and not S-RCDDEPTH, S-RCD-WIDTH, or S-RCD-PERM), and vice versa.

Proof: Straightforward induction on derivations.

Lemma 16.1.1 justifies eliminating rules S-RCDDEPTH, S-RCD-WIDTH, and S-RCD-PERM in favor of S-RCD. Figure 16-1 summarizes the resulting system.

Figure 16-1: Subtype Relation with Records (Compact Version)

Next, we show that, in the system of Figure 16-1, the reflexivity and transitivity rules are inessential.

16.1.2 Lemma

1. S <: S can be derived for every type S without using S-REFL.

2. If S <: T is derivable, then it can be derived without using S-TRANS.

Proof: EXERCISE [RECOMMENDED, ⋆⋆⋆].

16.1.3 Exercise [⋆]

If we add the type Bool, how do these properties change?

This brings us to the definition of the algorithmic subtype relation.

16.1.4 Definition

The algorithmic subtyping relation is the least relation on types closed under the rules in Figure 16-2.

Figure 16-2: Algorithmic Subtyping

We say that the algorithmic rules are sound because every statement that can be derived from algorithmic rules can also be derived from the declarative rules (the algorithmic rules do not prove anything new), and complete because every statement that can be derived from the declarative rules can also be derived from the algorithmic rules (the algorithmic rules prove everything that could be proved before).

16.1.5 Proposition [Soundness and Completeness]

S <: T iff .

Proof: Each direction proceeds by induction on derivations, using one of the two previous lemmas.

Now the algorithmic rules, being syntax directed, can be read directly as an algorithm for checking the algorithmic subtype relation (and hence also the declarative subtype relation). In a more conventional pseudocode notation, the algorithm looks like this:

   subtype(S, T) = if T = Top, then true                   else if S = S1→S2 and T = T1→T2                     then subtype(T1, S1) ∧ subtype(S2, T2)                   else if S = {kj:Sj jÎ1..m} and T = {⌉i:Ti iÎ1..n}                     then  {⌉i iÎ1..n} ⊆ {kj jÎ1..m}                          ∧for all i there is some j Î 1..m with kj = ⌉i                             and subtype(Sj, Ti)                   else false. 

A concrete realization of this algorithm in ML appears in Chapter 17.

Finally, we need to verify that the algorithmic subtype relation is total-i.e., that the recursive function subtype derived from the algorithmic rules returns either true or false, for every pair of inputs, after a finite amount of time.

16.1.6 Proposition [Termination]

If is derivable, then subtype(S, T) will return true. If not, then subtype(S, T) will return false.

This theorem, together with the soundness and completeness of the algorithmic rules, essentially asserts that the subtype function is a decision procedure for the declarative subtype relation.

Proof: The first claim is easy to check (by a straightforward induction on a derivation of ). Conversely, it is also easy to check that, if subtype(S, T) returns true, then . Thus, to establish the second claim, it suffices to show that subtype(S, T) must always return something-i.e., that it cannot diverge. This we can do by observing that the sum of the sizes of the input pair S and T is always strictly larger than the sum of the sizes of the arguments to any recursive call that that algorithm makes. Since this sum is always positive, an infinite sequence of recursive calls is not possible.

The reader may wonder whether we could have saved ourselves all the work in this section by simply taking the algorithmic definition of the subtype relation as the official definition and never even mentioning the declarative version. The answer is a qualified "Yes." We can certainly take the algorithmic definition as the official one when defining the calculus, if we prefer. However, this does not actually save much work, because, to show that the typing relation (which depends on the subtype relation) is well-behaved, we will need to know that subtyping is reflexive and transitive, and these proofs involve more or less the same work as we have done here. (On the other hand, language definitions do often adopt an algorithmic presentation of the typing relation. We will see one example of this in Chapter 19.)

---