Subtype #
As we saw in the previous sections, the purpose of generic programming is to write abstract code while enforcing type constraints.
As a result, when we write a program that uses a generic type (e.g. a native Java Collection),
we need to make sure that our code complies with these type constraints.
In some situations, this requires reasoning about types and their hierarchy (notably for programs that use callback methods).
In this section, we briefly illustrate how the notion of a subtype extends to functions (and more generally, methods). This will allow us to understand (in the dedicated section) some type constraints expressed via generics in languages like Java or C#.
The subtype relation #
Intuitively, $A$ is a subtype of $B$ if “every $A$ is a $B$”.
Notation. We will use $A \sqsubseteq B$ to indicate that $A$ is a subtype of $B$.
Examples. In Java,
Integer$\sqsubseteq$Number,String$\sqsubseteq$Object.
In object-oriented programming, subtyping generalizes hierarchical relations between classes, interfaces, etc.
Example. In Java, $A \sqsubseteq B$ if:
- $A$ and $B$ are classes and $A$
extends$B$ (directly or transitively), or- $A$ and $B$ are interfaces and $A$
extends$B$ (directly or transitively), or- $A$ is a class, $B$ is an interface and $A$
implements$B$ (directly or transitively), or- etc.
Observation. “Subtype” is a binary relation. This relation is both:
reflexive: every type $A$ is a subtype of itself,
transitive: if $A$ is a subtype of $B$ and $B$ is a subtype of $C$, then $A$ is a subtype of $C$.
Observation. If an object $o$ has type $A$ and $A$ is a subtype of $B$, then $o$ also has type $B$.
Examples. In Java:
- if an object has type
Integer, then it also has typeNumber,- if an object has type
String, then it also has typeObject.
Method subtyping #
Question. How do the observations above generalize to methods and the types of their arguments and return value?
To answer this question, we will first use mathematical functions as an analogy, for simplicity.
Domain, codomain and set inclusion #
Reminder. A function $f\colon X \to Y$ maps every element of its domain $X$ to some element of its codomain $Y$.
Glossary (reminder).
- $\mathbb{N}$ : natural numbers (a.k.a. positive integers, including
0)- $\mathbb{Z}$ : integers
- $\mathbb{Q}$ : rational numbers
Observe that $\mathbb{N} \subseteq \mathbb{Z} \subseteq \mathbb{Q}$.
Example. Consider the function $\mathit{population}$ that maps an Italian city to its population (i.e. number of inhabitants), and let $\mathit{ItalianCities}$ denote the set of all Italian cities.
We can write
$\qquad \mathit{population}\,\colon \mathit{ItalianCities} \to \mathbb{N}$
because the function $\mathit{population}$ maps every Italian city to a natural number.
We can also write
$\qquad \mathit{population}\,\colon \mathit{ItalianCities} \to \mathbb{Z}$
because it maps every Italian city to an integer (since natural numbers are integers).
For the same reason, we can also write
$\qquad \mathit{population}\,\colon \mathit{ItalianCities} \to \mathbb{Q}$
However, we cannot write
$\qquad \mathit{population}\,\colon \mathit{Cities} \to \mathbb{N}$
because it does not map every city (only Italian ones).
Method type #
Simple method types are analogous to the domains and codomains of functions:
Definition. A method has type $X \to Y$ if it accepts as input any element with type $X$, and returns an element with type $Y$.
Exercises #
Imagine a programming language that supports arbitrary rationals, integers and natural numbers (e.g. this can be simulated in Java with the java.math library).
In this language, we naturally have $\mathbb{N} \sqsubseteq \mathbb{Z} \sqsubseteq \mathbb{Q}$.
Now consider a method $f$ with type $\mathbb{Q} \to \mathbb{Q}$ that:
- takes as input a number $x$, and
- returns $x^2$.
Which of the following types are also valid for $f$ ?
- $\qquad \mathbb{Q} \to \mathbb{Z}$
- $\qquad \mathbb{Q} \to \mathbb{N}$
- $\qquad \mathbb{Z} \to \mathbb{Q}$
- $\qquad \mathbb{Z} \to \mathbb{Z}$
- $\qquad \mathbb{Z} \to \mathbb{N}$
- $\qquad \mathbb{N} \to \mathbb{Q}$
- $\qquad \mathbb{N} \to \mathbb{Z}$
- $\qquad \mathbb{N} \to \mathbb{N}$
3, 4, 5, 6, 7, 8
In our imaginary language, which of the following are correct?
A method with type $\mathbb{Z} \to \mathbb{Z}$ also has type:
- $\qquad \mathbb{N} \to \mathbb{N}$
- $\qquad \mathbb{N} \to \mathbb{Z}$
- $\qquad \mathbb{N} \to \mathbb{Q}$
- $\qquad \mathbb{Z} \to \mathbb{N}$
- $\qquad \mathbb{Z} \to \mathbb{Q}$
- $\qquad \mathbb{Q} \to \mathbb{N}$
- $\qquad \mathbb{Q} \to \mathbb{Z}$
- $\qquad \mathbb{Q} \to \mathbb{Q}$
2, 3, 5
Generalization #
We can now generalize these observations:
Property. $X_1 \sqsubseteq X_2$ and $Y_1 \sqsubseteq Y_2$ imply
$\qquad X_2 \to Y_1 \sqsubseteq X_1 \to Y_2$
Example. If
Butterfly$\sqsubseteq$Unit, then a Java method with typeUnit$\to$Integeralso has type:
Butterfly$\to$IntegerUnit$\to$NumberButterfly$\to$Number