We use the notation $S <: T$ to denote the fact that type $S$ is a sub type of $T$, meaning that every value described by $S$ is also described by $T$. The bridge between the typing relation and this subtype relation is provided by adding a new typing rule, dubbed “subsumption”:

$$ \frac{\Gamma \vdash a: S, S<:T}{\Gamma \vdash a: T} = \mathtt{T-Sub} $$

We can also introduce some interesting facts about the sub-typing rules:

$$ \frac{}{S <: S} = \mathtt{S-Refl} \\ $$

$$ \frac{S <: T, T<:U}{S <: U} = \mathtt{S-Trans} $$

$$ \frac{S_1<:T_1, S_2 <: T_2}{S_1 \to S_2 <: T_1 \to T_2} = \mathtt{S-Arrow} $$

Also, we can define some “top” type $\top$ which serves as the parent for all types. Similarly we can define a bottom type that serves as a sink.

$$ \frac{\forall S: \mathcal{U}}{S <: \top} = \mathtt{S-Top} $$

$$ \frac{S: \mathcal{U}}{\bot <: S} = \mathtt{S-Bot} $$

By introducing the notion of subtyping, the STLC is more expressive to represent most real-world applications.

Let us try to prove the following simple inversion lemma:

If $S <: T_1 \to T_2$, then $S$ has the form $S_1 \to S_2$ with $T_1 <: S_1$ and $T_2 <: S_2$.

Proof. By induction on the derivation rule, we know that to obtain $S <: T_1 \to T_2$, there are three possible cases: S-Refl, S-Trans, and S-Arrow. We analyze each case as follows.

• S-Refl: In this case the result is obvious, since $S \equiv T_1 \to T_2$ with $T_1 <: T_1$ and $T_2 <: T_2$.
• S-Trans: In this case we know that there exists some $U$ such that $U <: T_1 \to T_2$ and $S <: U$. We apply the induction hypothesis so that we can obtain the fact that $U$ must have the form $U_1 \to U_2$ with $T_1 <: U_1$ and $T_2 <: U_2$. Thus $S <: U_1 \to U_2$. Applying the induction hypothesis again we know that $S$ has the form $S_1 \to S_2$ with $U_1 <: S_1$ and $U_2 <: S_2$. Applying S-Trans for $U_1 <: S_1$ and $T_1 <: U_1$ we know that $T_1 <: S_1$ and $T_2 <: S_2$.
• S-Arrow: Trivial.