These notes review our discussion of subsumption and subtyping in type-and-effect systems.

Our discussion of type and effect systems included
the *subsumption* rule.

This rule should seem counter-intuitive: the conclusion has more effects---that is, makes a weaker statement about the term $e$---that the premises. And, in the absense of abstraction, we could mostly work around the need for subsumption. But once we introduction abstractions (i.e., functions), subsumption becomes unavoidable. Consider the following example:

if isz x then throw[Int] else get - x

The two branches of the `if`

have different effects, so these effects must be merged
in the type of the expression. We have written the typing rule for `if`

to take this
possibility into account, and so we can conclude that this example has type $Int
\stackrel{\{\mathsf{ex,read}\}}\to Int$. However, if we add an extra layer of abstraction, we
have a problem:

if isz x then \y : 1 -> throw[Int] else \y : 1 -> get - x

Now, the naive derivations of the two branches are $$ x : \Int \vdash \backslash y : 1 \to \Throw{\Int} : \Int \stackrel{\{\mathsf{ex}\}}\to \Int \With \emptyset $$ and $$ x : \Int \vdash \backslash y : 1 \to \Get : \Int \stackrel{\{\mathsf{read}\}}\to \Int \With \emptyset $$ The problem is no longer that the effects do not match, but that the types themselves do not match. To construct a typing for this term, we need to use the subsumption rule in the derivation of each branch, to conclude that they can both have the type $\Int \stackrel{\{\mathsf{ex,read}\}}\to \Int$.

If that were as far as it went, this would not be too bad. But consider another example. Suppose that $g_1$ has type $(\Int \stackrel{\Set{\Ex}}\to \Int) \stackrel{z}{\to} 1$ and $g_2$ has type $(\Int \stackrel{\Set{\Read}}\to \Int) \stackrel{z}{\to} 1$, and consider the term

let f = \x : Int -> x in if isz y then g_{1}f else g_{2}f

Now, we have a problem. If we inline the body of `f`

in the two branch of
the `if`

statement, then the resulting term can type. In the first branch, we use
subsumption to conclude that `\x : Int -> x`

has type $\Int \stackrel{\Set{\Ex}}\to
\Int$, and in the second branch that it has type $\Int \stackrel{\Set{\Read}}\to \Int$. But we
cannot give `f`

a single type that encompasses both of these uses, and so it seems
that we cannot type this term.

The key relationship that we need to capture is one among types, corresponding to (hypothetical)
uses of the subsumption rule. This is an example of a more general pattern
called *subtyping*, which appears throughout programming languages, particularly in
object-oriented programming languages.

To capture this relationship, we start by introducing a new relation on types, $t_1 \Sub t_2$.
The intuition behind this relation is that any time you expect a value of type $t_2$, you can
substitute a value of type $t_1$. An alternative view is that the values of type $t_1$ are a
subset of the values of type $t_2$. For example, suppose we had a type `Pos`

that
contained only the positive integers. Then, we would have that $\mathtt{Pos} \Sub
\mathtt{Int}$.

We can formally define the $\Sub$ relation using natural deduction rules, as follows.

$$ \frac{ }{\Int \Sub \Int} \quad \frac{ }{\Bool \Sub \Bool} $$The base types are subtypes only of themselves.

$$ \frac{t_1 \Sub t_2 \quad u_1 \Sub u_2} {t_1 \times u_1 \Sub t_2 \times u_2} \quad \frac{t_1 \Sub t_2 \quad u_1 \Sub u_2} {t_1 + u_1 \Sub t_2 + u_2} $$Product and sum types are subtypes if their components are subtypes. Consider the product types: if $t_1 \times u_1 \Sub t_2 \times t_2$, then we expect to be able to use a $t_1 \times u_1$ value anywhere we expect a $t_2 \times u_2$ value. What does this mean? The primary thing we can do with a term of product type is to access its components, so it must be the case that the components of the $t_1 \times u_1$ value can be used where the components of the $t_2 \times u_2$ value are expected. The intuition for sums is similar.

$$ \frac{t_2 \Sub t_1 \quad u_1 \Sub u_2 \quad z_1 \subseteq z_2} {t_1 \stackrel{z_1}{\to} u_1 \Sub t_2 \stackrel{z_2}{\to} u_2} $$Functions are the interesting case. Suppose that $t_1 \stackrel{z_1}{\to} u_1 \Sub t_2 \stackrel{z_2}{\to} u_2$; this means that we should be able to use a function of type $t_1 \stackrel{z_1}{\to} u_1$ any time we expect a function of type $t_2 \stackrel{z_2}{\to} u_2$. What does this require? It requires that the result $u_1$ be usable wherever we expected a result $u_2$, so $u_1 \Sub u_2$; it also requires that the effects $z_1$ be no more than the expected effects $z_2$, so $z_1 \subseteq z_2$. Finally, it requires that any argument valid for $t_2 \stackrel{z_2}{\to} u_2$ also be valid for $t_1 \stackrel{z_1}{\to} u_1$; that is, that $t_2 \Sub t_1$. Note that this is reversed from the other relations.

Having defined the subtyping relation, we need to introduce it to the type system. As with subsumption, the most straightforward way to do so is by introducing a new typing rule.

$$ \frac{\Gamma \vdash e : t' \quad t' \Sub t} {\Gamma \vdash e : t} $$This captures the intuition of subtyping directly: any time you need a term of type $t$, a term of type $t'$ will do.

However, from an implementation perspective, this rule is problematic. Up to this point, our
type systems have been *syntax-directed*. That is, the typing rule to be applied at each
point is determined by the syntax of the term. This is not true for the subtyping (or
subsumption) rules: they can be applied at any point in a derivation. However, we do not want
to over-eagerly apply subtyping or subsumption, as doing so loses information about the term.

To resolve this problem, we observe that, while we *could* apply subtyping at arbitrary
points, it is only necessary to do so when we are comparing types for equality. This leads us
to an alternative approach, in which we do not include the subtyping rule in its full
generality, but instead build subtyping into the other rules where it could usefully be applied.