LARA

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.