16.2 Algorithmic Typing

---

16.2 Algorithmic Typing

Having gotten the subtype relation under control, we need to do the same with the typing relation. As we saw on page 209, the only non-syntax-directed typing rule is T-SUB, so this is the one we must deal with. As with S-TRANS in the previous section, we cannot simply delete the subsumption rule: we must first examine where it plays a critical role in typing and enrich the other typing rules to achieve the same effects in a more syntax-directed way.

Clearly, one critical use of subsumption is bridging gaps between the types expected by functions and the actual types of their arguments. A term like

   (λr:{x:Nat}. r.x) {x=0,y=1} 

is not typable without subsumption.

Perhaps surprisingly, this is the only situation where subsumption plays a crucial role in typing. In every other case where subsumption is used in a typing proof, the same statement can be proved by a different derivation in which subsumption is "postponed" by moving it down the tree toward the root. To see why this works, it is instructive to experiment a little with typing derivations involving subsumption, taking each typing rule in turn and thinking about how a derivation ending with this rule can be reorganized if one of its immediate subderivations ends with T-SUB.

For example, suppose we are given a typing derivation ending with T-ABS, whose immediate subderivation ends with T-SUB.

Such a derivation can be rearranged so that subsumption is used after the abstraction rule to achieve the same conclusion:

A more interesting case is the application rule T-APP. Here there are two subderivations, either of which might end with T-SUB. Consider first the case where subsumption appears at the end of the left-hand subderivation.

From the results in the previous section, we may assume that the final rule in the derivation of S₁₁→S₁₂ <: T₁₁→T₁₂ is neither S-REFL nor S-TRANS. Given the form of its conclusion, this rule can then only be S-ARROW.

Rewriting to eliminate the instance of T-SUB has an interesting effect.

The right-hand subderivation of the original instance of S-ARROW has been pushed down to the bottom of the tree, where a new instance of T-SUB raises the type of the whole application node. On the other hand, the left-hand sub-derivation has been pushed up into the derivation for the argument s₂.

Suppose instead that the instance of T-SUB that we want to relocate occurs at the end of the right-hand subderivation of an instance of T-APP.

The only thing we can do with this instance of T-SUB is to move it over into the left-hand subderivation-partly reversing the previous transformation.

So we see that the use of subsumption for promoting the result type of an application can be moved down past the T-APP rule, but that the use of subsumption for matching the argument type and the domain type of the function cannot be eliminated. It can be moved from one premise to the other-we can promote the type of the argument to match the domain of the function, or we can promote the type of the function (by demoting its argument type) so that it expects an argument of the type we actually plan to give it-but we cannot get rid of the subsumption altogether. This observation corresponds precisely with our intuition that this gap-bridging use of subsumption is essential to the power of the system.

Another case we have to consider is where the last rule in a derivation is subsumption and its immediate subderivation also ends with subsumption. In this case, the two adjacent uses of subsumption can be coalesced into one-i.e., any derivation of the form

can be rewritten:

16.2.1 Exercise [⋆ ↛]

To finish the experiment, show how to perform similar rearrangements on derivations in which T-SUB is used before T-RCD or T-PROJ.

By applying these transformations repeatedly, we can rewrite an arbitrary typing derivation into a special form where T-SUB appears in only two places: at the end of right-hand subderivations of applications, and at the very end of the whole derivation. Moreover, if we simply delete the one at the very end, no great harm will result: we will still have a derivation assigning a type to the same term-the only difference is that the type assigned to this term may be a smaller (i.e., better!) one. This leaves just one place, applications, where uses of subsumption can still occur. To deal with this case, we can replace the application rule by a slightly more powerful one

incorporating a single instance of subsumption as a premise. Every subderivation of the form application-preceded-by-subsumption can be replaced by a use of this rule, which leaves us with no uses of T-SUB at all. Moreover, the enriched application rule is syntax directed: the shape of the term in the conclusion prevents it from overlapping with the other rules.

This transformation yields a syntax-directed set of typing rules that assigns types to the same terms as the original typing rules. These rules are summarized in the following definition. As we did for the algorithmic subtyping rules, we write the algorithmic relation with a funny turnstile, , to distinguish it from the declarative relation.

16.2.2 Definition

The algorithmic typing relation is the least relation closed under the rules in Figure 16-3. The premise T₁ = T₁₁→T₁₂ in the application rule is simply an explicit reminder of the sequencing of operations during typechecking: first we calculate a type T₁ for t₁; then we check that T₁ has the form T₁₁→T₁₂, etc. The rule would have exactly the same force if we dropped this premise and instead wrote the first premise as . Similarly for TA-PROJ. Also, the subtyping premise in the application rule is written with a funny turnstile; since we know that the algorithmic and declarative presentations of subtyping are equivalent, this choice is a matter of taste.

Figure 16-3: Algorithmic Typing

16.2.3 Exercise [⋆ ↛]

Show that the type assigned to a term by the algorithmic rules can decrease during evaluation by finding two terms s and t with algorithmic types S and T such that s →* t and T <: S, but S ≮: T.

We now need to check formally that the algorithmic typing rules correspond to the original declarative rules. (The transformations on typing derivations that we enumerated above are too informal to be considered a proof. They could be turned into one, but it would be longer and heavier than necessary: it is simpler just to argue by induction on derivations, as usual.) As we did for subtyping, we argue that the algorithmic typing relation is both sound and complete with respect to the original declarative rules.

The soundness property is unchanged: every typing statement that can be derived from the algorithmic rules also follows from the declarative rules.

16.2.4 Theorem [Soundness]

If . then Г ⊢ t : T.

Proof: Straightforward induction on algorithmic typing derivations.

Completeness, though, looks a little different. The ordinary typing relation can be used to assign many types to a term, while the algorithmic typing relation assigns at most one (as can easily be checked). So a straightforward converse of Theorem 16.2.4 is clearly not going to hold. Instead, we can show that if a term t has a type T under the ordinary typing rules, then it has a better type S under the algorithmic rules, in the sense that S <: T. In other words, the algorithmic rules assign each typable term its smallest possible (minimal) type. The completeness theorem is often called the Minimal Typing theorem, since (when combined with Theorem 16.2.4) it amounts to showing that each typable term in the declarative system has a minimal type.

16.2.5 Theorem [Completeness, or Minimal Typing]

If Г ⊢ t : T, then for some S <: T.

Proof: EXERCISE [RECOMMENDED, ⋆⋆].

16.2.6 Exercise [⋆⋆]

If we dropped the arrow subtyping rule S-Arrow but kept the rest of the declarative subtyping and typing rules the same, would the system still have the minimal typing property? If so, prove it. If not, give an example of a typable term with no minimal type.

---