# 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