Subtype Relation

type-theory

Definition

Subtype Relation

The subtype relation is a partial order, often denoted as $S<:T$ or $S\le T$, meaning type $S$ is a subtype of type $T$, where $T$ is called supertype of $S$. It signifies that any term or value of type $S$ can be safely used in any context where a term or value of type $T$ is expected. This is known as the principle of substitutability.

Language-Specific

Java

Let $T,S,R$ be reference types.

• $T\le T$ (reflexive)
• $R\le S\wedge S\le T⟹R\le T$ (transitive)
• $S\le T\wedge T\le S⟹S=T$ (antisymmetric)

Thus, the subtype relation is a partial order.

• $S\text{ is interface}\wedge S\le T⟹T\text{ is interface}$
• $T\text{ is class}\wedge S\le T⟹S\text{ is class}$
• $T\text{ is class}⟹T\le \text{java.lang.Object}$
• Every dynamic type is a Java class
• $\text{null}$ is not an object of $T$, whereby the compiler accepts it

Assumption: Method comments in $S$ and $T$ are compatible, with $S\le T$:

• Comment in $S$ explains the same method as comment in $T$
• Comment in $S$ can be more concrete
• Comment in $T$ can be more abstract