Types and Programming Languages Chapter 16 Metatheory of Subtyping

And so it was that on the 19th of September, the Year of our Lord 2017, the Computation Club of London met with every intention of blasting through The Metatheory of Subtyping. Per Tom's chapter update:

It’s called “Metatheory of Subtyping”, making it perhaps the most intimidatingly-titled chapter we’ve seen so far, which is unfortunate because it’s actually quite practical and engineering-y. Of course we have to wade through the usual mathematical language to get to the practical engineering bits, but ultimately the chapter could’ve easily been called “Actually Implementing Subtyping: How Do You Flipping Even?” if Piercey Pierce hadn’t been so keen to impress at parties.

We like to think of ourselves as quite practical and engineering-y, so how did we get on? PROBABLY FINE, RIGHT! Basically we had this one pencilled in as a gimme.

Unfortunately, as you probably already know, computers.

Background / motivation

We spent a moment recapping why subtyping presents a problem for implementation at all. Tom said:

The typing rules we saw in chapter 15 are like great and everything, but they’re not in a fit state to be directly implemented as a typechecking algorithm. The T-Sub rule (from the typing relation) has such a vague conclusion that it can be applied to any term; the S-Trans rule (from the subtyping relation) has the same problem, plus it expects us to somehow invent an intermediate type when gluing two other subtyping derivations together. In both cases the necessary “guesswork” makes the previously syntax-directed process of typechecking much less obvious. We have coped with this during whiteboarding sessions by using intuition to decide which rules to apply at which points, but that’s not good enough for a computer is it? Let’s sort it! Get out of my pub!

We spent a bit of time discussing what the implications of this were for implementation algorithms. Previously our inference rules for the different relations (typing, evaluation...) had been so mechanical and so reductive that we could turn them more-or-less directly into an algorithm to derive the relation they described.

For example, T-Abs is applicable only to lambda abstractions, and the single premise is such that we know we're type-checking a smaller term (i.e. the body of the lambda abstraction):

   Γ,x:T1 ⊢ t2 : T2
----------------------
Γ ⊢ λx:T1.t2 : T1 → T2

By contrast, the new T-Sub rule is not so restrictive - it applies to literally any term:

Γ ⊢ t : S, S <: T
-----------------
   Γ ⊢ t : T

Up until now our implementations have effectively been a big case statement for different sorts of terms:

def type_of(term, context = {})
  case term
  when Term::True, Term::False
    # ...
  when Term::Var
    # ...
  when Term::Abs
    # ...
  when Term::If

With T-Sub we've got no such restriction - the bare metavariable t will match any term, and as it appears directly in the premise (Γ ⊢ t : S) we could end up executing this rule forever if we implemented it directly as written. Until now our rules have been syntax-directed, which is to say that each rule has matched a single syntactic form, meaning at any given point we always know which rule to apply. That's no longer the case!

With the subtyping relation, this is even more troublesome - not only do we have a bare metavariable S in the conclusion, we have a completely new intermediate variable U in the premises:

S <: U   U <: T
---------------
    S <: T

When considering this rule before we've intuited U using our enormous human brains, but that doesn't really work for programming, more's the pity. The rest of the chapter discusses elegant logical workarounds / appalling hacks around the above problems, which let us turn the above inference rules back into something syntax-directed.

16.1 Algorithmic Subtyping

16.2 Algorithmic Typing