Subtype Relation

type-theory

Definition

Subtype Relation

Let $A$ and $B$ be types. $A$ is called subtype of $B$, denoted as $A\le B$, if anywhere where an expression of type $B$ is expected, an expression of type $A$ can be safely used (Liskov Substitution Principle).

The subtype relation forms a partial order.

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

Object-Oriented Perspective

A type $U$ is subtype of type $T$ iff:

1. $\forall c_T\in \text{constants}(T):\exists c_U\in \text{constants}(U):\text{type}(c_U)\le \text{type}(c_T)$
   1. i.e. type of $c_U$ is subtype of type $c_T$
2. $\forall v_T\in \text{vars}(T):\exists v_U\in \text{vars}(v_U):\text{type}(v_T)\equiv \text{type}(v_U)$
   1. i.e. type of $v_T$ is equivalent to type $v_U$
3. $\forall m_T\in \text{methods}(T):\exists m_U\in \text{methods}(U):$
   1. parameter count and types are equal
   2. parameter types are compatible
   3. result type of $m_T$ is subtype of result type in $m_U$
   4. $m_U$ does not throw more exceptions than $m_T$