Types and Programming Languages

31.3 Properties

Proofs of fundamental properties of , including preservation of types during reduction, progress, and minimal typing, for (a near relative of) this system can be found in the papers cited at the beginning of the chapter. These proofs must, of course, address all the issues raised by subtyping, bounded quantification, and type operators in isolation. In addition, one significant new complication arises when we try to define an alternative, syntax-directed presentation of the subtyping rules: not only can the type variable rule be used in combination with transitivity in an essential way in subtyping derivations (as we saw in §28.3), but so can type equivalence (rule S-EQ) together with transitivity.

For example, in the context Г = X<:Top, F<:λY.Y, the statement Г ⊢ F X <: X is provable as follows (ignoring kinding):

Moreover, note that we cannot get around this interaction simply by reducing all type expressions to their normal forms, since the expression F A is not a redex—it only becomes one when, during subtype checking, the variable F is promoted to its upper bound λY.Y. The solution is to normalize type expressions once at the beginning of the subtype check and then re-normalize as necessary during the promotion operation.