21.3 Subtyping

---

21.3 Subtyping

We define subtype relations on finite tree types and on tree types in general as least and greatest fixed points, respectively, of monotone functions on certain universes. For subtyping on finite tree types the universe is the set T_f × T_f of pairs of finite tree types; our generating function will map subsets of this universe—that is, relations on T_f—to other subsets, and their fixed points will also be relations on T_f. For subtyping on arbitrary (finite or infinite) trees, the universe is T × T.

21.3.1 Definition [Finite Subtyping]

Two finite tree types S and T are in the subtype relation ("S is a subtype of T") if (S, T) Î μS_f , where the monotone function S_f Î P(T_f × T_f) → P(T_f × T_f) is defined by

•  

  Sf(R)	=	{(T, Top) | T Î Tf}
  	È	{(S1 × S2, T1 × T2) | (S1, T1), (S2, T2) Î R}
  	È	{(S1 → S2, T1 → T2) | (T1, S1), (S2, T2) Î R}.

This generating function precisely captures the effect of the standard definition of the subtype relation by a collection of inference rules:

The statement S <: T above the line in the second and third rules should be read as "if the pair (S, T) is in the argument to S_f" and below the line as "then (S, T) is in the result."

21.3.2 Definition [Infinite Subtyping]

Two (finite or infinite) tree types S and T are in the subtype relation if (S, T) Î vS, where S Î P(T × T) → P(T × T) is defined by:

•  

  S(R)	=	{(T, Top) | T Î T}
  	È	{(S1 × S2, T1 × T2) | (S1, T1), (S2, T2) Î R}
  	È	{(S1 → S2, T1 → T2) | (T1, S1), (S2, T2) Î R}.

Note that the inference rule presentation of this relation is precisely the same as for the inductive relation above: all that changes is that we consider a larger universe of types and take a greatest instead of a least fixed point.

21.3.3 Exercise [⋆]

Check that vS is not the whole of T × T by exhibiting a pair (S, T) that is not in vS.

21.3.4 Exercise [⋆]

Is there a pair of types (S, T) that is related by vS, but not by μS? What about a pair of types (S, T) that is related by vS_f, but not by μS_f?

One fundamental property of the subtype relation on infinite tree types— the fact that it is transitive—should be verified right away. (We have already seen in §16.1 that subtyping on finite types is transitive.) If the subtype relation were not transitive, the critical property of preservation of types under evaluation would immediately fail. To see this, suppose that there were types S, T, and U with S<:T and T<:U but not S<:U. Let s be a value of type S and f a function of type U→Top. Then the term (λx:T. f x) s could be typed, using the rule of subsumption once for each application, but this term reduces in one step to the ill-typed term f s.

21.3.5 Definition

A relation R ⊆ U × U is transitive if R is closed under the monotone function TR(R) = {(x, y) | $z Î U. (x, z), (z, y) Î R}—i.e., if TR(R) ⊆ R.

21.3.6 Lemma

Let F Î P(U×U) → P(U×U) be a monotone function. If TR(F(R)) ⊆ F(TR(R)) for any R ⊆ U × U, then vF is transitive.

Proof: Since vF is a fixed point, vF = F(vF), implying TR(vF) = TR(F(vF)). Therefore, by the lemma's assumption, TR(vF) ⊆ F(TR(vF)). In other words, TR(vF) is F-consistent, so, by the principle of coinduction, TR(vF) ⊆ vF. Equivalently, vF is transitive by Definition 21.3.5.

This lemma is reminiscent of the traditional technique for establishing redundancy of the transitivity rule in inference systems, often called "cut-elimination proofs" (see §16.1). The condition TR(F(R)) ⊆ F(TR(R)) corresponds to the crucial step in this technique: given that a certain statement can be obtained by taking some statements from R, applying rules from F, and then applying the rule of transitivity TR, we argue that the statement can instead be obtained by reversing the steps—first applying the rule of transitivity, and then rules from F. We use the lemma to establish transitivity of the subtype relation.

21.3.7 Theorem

vS is transitive.

Proof: By Lemma 21.3.6, it suffices to show that TR(S(R)) ⊆ S(TR(R)) for any R ⊆ T × T. Let (S, T) Î TR(S(R)). By the definition of TR, there exists some U Î T such that (S, U), (U, T) Î S(R). Our goal is to show that (S, T) Î S(TR(R)). Consider the possible shapes of U.

Case:

U = Top

Since (U, T) Î S(R), the definition of S implies that T must be Top. But (A, Top) Î S(Q) for any A and Q; in particular, (S, T) = (S, Top) Î S(TR(R)).

Case:

U = U₁ × U₂

If T = Top, then (S, T) Î S(TR(R)) as in the previous case. Otherwise, (U, T) Î S(R) implies T = T₁ × T₂, with (U₁, T₁), (U₂, T₂) Î R. Similarly, (S, U) Î S(R) implies S = S₁ × S₂, with (S₁, U₁), (S₂, U₂) Î R. By the definition of TR, we have (S₁, T₁), (S₂, T₂) Î TR(R), from which (S₁ × S₂, T₁ × T₂) Î S(TR(R)) follows from the definition of S.

Case:

U = U₁ → U₂

Similar.

21.3.8 Exercise [Recommended, ⋆⋆]

Show that the subtype relation on infinite tree types is also reflexive.

The following section continues the discussion of transitivity by comparing its treatment in standard accounts of subtyping for finite types and in the present account of subtyping for infinite tree types. It can be skipped or skimmed on a first reading.

---