# 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