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