# 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 as approximating the set of values to which an expression can evaluate

• statement corresponds to

What are the sets like?

• in previous systems, distinct types denoted disjoint sets: if then
• in more complex systems, these sets overlap

We write , saying s is a subtype of t to correspond to

For function types, we assume that functions are defined on all arguments and that means

There are type systems that have intersections and unions, roughly corresponding to and

## Subtyping as a Syntactic Notion

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

• and

then also

Two ways to ensure the weakening rule:

First way: introduce explicitly a general subtyping rule

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

Introduce 'pos' with

and 'neg' with

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 ):

for every

for every

for every

Let denote arithmetic expressions.

Some of the rules:

For every type ,

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)

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