Subtyping

Definition

Consider a type system with a typing relation $\Gamma \vdash t : T$, such as the simply typed lambda calculus extended with record types $\set{l_1 : T_1, \dots, l_n : T_n}$ with distinct labels $l_i$. A subtyping relation is a relation $S <: T$ on types that is closed under these rules.

1. Reflexivity: $T <: T$.
2. Transitivity: if $S <: U$ and $U <: T$, then $S <: T$.
3. Functions: if $T_1 <: S_1$ and $S_2 <: T_2$, then $S_1 \to S_2 <: T_1 \to T_2$.
4. Records: $\set{l_1 : S_1, \dots, l_n : S_n} <: \set{k_1 : T_1, \dots, k_m : T_m}$ if each label $k_j$ equals some label $l_i$, and $S_i <: T_j$ for that $i$.

The type system is linked to $<:$ by the subsumption rule: if $\Gamma \vdash t : S$ and $S <: T$, then $\Gamma \vdash t : T$. The relation $<:$ is usually taken to be the least relation closed under the rules, together with chosen relations between base types, such as $\mathsf{Int} <: \mathsf{Real}$.