31.2 Definitions

---

31.2 Definitions

The rules defining are listed in Figure 31-1. One technicality in the definition is that, although the system provides two different sorts of binding for type variables (X::K in type operators and X<:T in quantifiers), we allow only the latter form of binding in contexts. When we move an X::K binder from the right-hand side of the turnstile to the left, in rules K-ABS and S-ABS, we change it to X<:Top[K].

Another fine point is that the rules S-REFL from F_<: and T-EQ from F_ω are dropped in . Instances of the old S-REFL are immediate consequences of S-EQ and Q-REFL, while T-EQ is derivable from T-SUB and S-EQ.

31.2.1 Exercise [⋆]

If we define Id = λX.X and

   Г = B<:Top, A<:B, F <: Id 

then which of the following subtype statements are derivable?

    Г  ⊢  A                         <:  Id B    Г  ⊢  Id A                      <:  B    Г  ⊢  λX.X                      <:  λX.Top    Г  ⊢  λX. "Y<:X. Y              <:  λX. "Y<:Top. Y    Г  ⊢  λX. "Y<:X. y              <:  λX. "Y<:X. X    Г  ⊢  FB                        <:  B    Г  ⊢  B                         <:  FB    Г  ⊢  FB                        <:  FB    Г  ⊢  "F<:(λY.Top→Y). FA        <:  "F<:(λY.Top→Y). Top→B    Г  ⊢  "F<:(λY.Top→Y). FA        <:  "F<:(λY.Top→Y). F B    Г  ⊢  Top[*⇒*]                  <:  Top[*⇒*⇒*] 

---