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

Illustrative Example: 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

$\begin{equation*} pos <: int \end{equation*}$

and

$\begin{equation*} neg <: int \end{equation*}$

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.

Moreover, we can type check e.g. operations on fractions represented as a pair (p,q) of integer p and a positive integer q, with the meaning p/q :

def multiplyFractions(p1 : int, q1 : pos, p2 : int, q2 : pos) : (int,pos) {
  (p1*q1, q1*q2)
}
def addFractions(p1 : int, q1 : pos, p2 : int, q2 : pos) : (int,pos) {
  (p1*q2 + p2*q1, q1*q2)
}
def printApproxValue(p : int, q : pos) = {
  print(p/q) // no division by zero
}

More sophisticated types can track intervals of numbers and ensure that a program does not crash with an array out of bounds error.