Notion of Subtyping

Subtypes as Subsets

In systems we have formally studied so far, each expression had exactly one type, such as 'int' or 'int → bool'

this is not case any more in systems with subtyping

We can often think of a type $t$ as approximating the set of values $V_t$ to which an expression can evaluate

statement $x:t$ corresponds to $x \in V_t$

What are the sets $V_t$ like?

in previous systems, distinct types denoted disjoint sets: if $s \neq t$ then $V_s \cap V_t = \emptyset$
in more complex systems, these sets overlap

We write $s <: t$ , saying s is a subtype of t to correspond to $V_s \subseteq V_t$

For function types, we assume that functions are defined on all arguments and that $f : s \to t$ means

$\begin{equation*} \forall x. x \in V_s \rightarrow f(x) \in V_t \end{equation*}$

There are type systems that have intersections and unions, roughly corresponding to $\cap$ and $\cup$

Subtyping as a Syntactic Notion

We treat $s <: t$ as a (potentially arbitrary) relation on the set of types, but we aim to define type system such that the following 'weakening' rule holds:

$s <: t$ and
$\Gamma \vdash e:s$

then also $\Gamma \vdash e:t$

Two ways to ensure the weakening rule:

First way: introduce explicitly a general subtyping rule

$\begin{equation*} \frac{\Gamma \vdash e:s, \ \ s <: t} {\Gamma \vdash e:t} \end{equation*}$

Second way: construct the remaning rules so that the subtyping rule follows as a consequence

In any case, we can use the same general methodology for Proving Safety Properties using Types

the meaning of type is 'something that makes program type check'
by soundness, if program type checks, then program has some good properties

Example: Expressions with Positive and Negative Integer Types

Suppose that we have arbitrary-precision integers denoted by 'int'. Then

$\begin{equation*} V_{int} = \{ \ldots, -2, -1, 0, 1, 2, \ldots \} \end{equation*}$

Introduce 'pos' with

$\begin{equation*} V_{pos} = \{ 1, 2, \ldots \} \end{equation*}$

and 'neg' with

$\begin{equation*} V_{neg} = \{ -1, -2, \ldots \} \end{equation*}$

Suppose int,pos,neg are the only types

We have pos<:int and neg<:int

Assuming that $+,-,*,/$ are special constructs (and not just variables as in lambda calculus), we have the following rules (fixing some environment $\Gamma$ ):

$\overline{n}:neg$ for every $n < 0$

$\overline{n}:pos$ for every $n > 0$

$\overline{n}:int$ for every $n$

Let $x,y$ denote arithmetic expressions.

Some of the rules:

$\begin{equation*} \frac{x:pos, y:pos} {x+y : pos} \end{equation*}$

$\begin{equation*} \frac{x:neg, y:neg} {x+y : neg} \end{equation*}$

$\begin{equation*} \frac{x:pos, y:neg} {x+y : int} \end{equation*}$

$\begin{equation*} \frac{x:pos, y:pos} {x*y : pos} \end{equation*}$

$\begin{equation*} \frac{x:pos, y:neg} {x*y : neg} \end{equation*}$

$\begin{equation*} \frac{x:neg, y:neg} {x*y : pos} \end{equation*}$

For every type $t$ ,

$\begin{equation*} \frac{x:t, y:pos} {x/y : t} \end{equation*}$

$\begin{equation*} \frac{x:t, y:neg} {x/y : t} \end{equation*}$

Note that these rules will prevent division by zero

What if we wish to check whether an integer is positive or negative?

introduce ifpos and ifneg operations:
(ifpos x y z) evaluates to y if x is positive and to z otherwise
inside y, we know that x is positive
here x must be a variable (not a complex expression)

$\begin{equation*} \frac{\Gamma \oplus \{x \mapsto pos\} \vdash y,\ \Gamma \vdash z} {\Gamma \vdash (ifpos\ x\ y\ z)} \end{equation*}$

Example: Expression

(ifpos x (y / x) (x + 1))

will never cause division by zero or any other arithmetic error

Note:

this tends to be not so nice to write, so e.g. Java uses exceptions to report such errors
a form of type inference can sometimes be used to show that exceptions cannot occur