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:
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 ):
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)
(ifpos x (y / x) (x + 1))
will never cause division by zero or any other arithmetic error
- 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