8.1.1. A Motivating Example🔗

Suppose we are writing a program involving two record types defined as follows:

      Person  = {name:String, age:Nat}
      Student = {name:String, age:Nat, gpa:Nat}

In the simply typed lamdba-calculus with records, the term

    (λ r:Person. (r.age)+1) {name="Pat", age=21, gpa=1}

is not typable, since it applies a function that wants a two-field record to an argument that actually provides three fields, while the app rule demands that the domain type of the function being applied must match the type of the argument precisely.

But this is silly: we're passing the function a better argument than it needs! The only thing the body of the function can possibly do with its record argument r is project the field age from it: nothing else is allowed by the type, and the presence or absence of an extra gpa field makes no difference at all. So, intuitively, it seems that this function should be applicable to any record value that has at least an age field.

More generally, a record with more fields is "at least as good in any context" as one with just a subset of these fields, in the sense that any value belonging to the longer record type can be used safely in any context expecting the shorter record type. If the context expects something with the shorter type but we actually give it something with the longer type, nothing bad will happen (formally, the program will not get stuck).

The principle at work here is called subtyping. We say that "σ is a subtype of τ", written σ <: τ, if a value of type σ can safely be used in any context where a value of type τ is expected. The idea of subtyping applies not only to records, but to all of the type constructors in the language -- functions, pairs, etc.

Safe substitution principle:

• σ is a subtype of τ, written σ <: τ, if a value of type σ can safely be used in any context where a value of type τ is expected.

8.1.2. Subtyping and Object-Oriented Languages🔗

Subtyping plays a fundamental role in many programming languages -- in particular, it is central to the design of object-oriented languages and their libraries.

An object in Java, C#, etc. can be thought of as a record, some of whose fields are functions ("methods") and some of whose fields are data values ("fields" or "instance variables"). Invoking a method m of an object o on some arguments a₁..an roughly consists of projecting out the m field of o and applying it to a₁..an.

The type of an object is called a class -- or, in some languages, an interface. It describes which methods and which data fields the object offers. Classes and interfaces are related by the subclass and subinterface relations. An object belonging to a subclass (or subinterface) is required to provide all the methods and fields of one belonging to a superclass (or superinterface), plus possibly some more.

The fact that an object from a subclass can be used in place of one from a superclass provides a degree of flexibility that is extremely handy for organizing complex libraries. For example, a GUI toolkit like Java's Swing framework might define an abstract interface Component that collects together the common fields and methods of all objects having a graphical representation that can be displayed on the screen and interact with the user, such as the buttons, checkboxes, and scrollbars of a typical GUI. A method that relies only on this common interface can now be applied to any of these objects.

Of course, real object-oriented languages include many other features besides these. For example, fields can be updated. Fields and methods can be declared "private". Classes can give initializers that are used when constructing objects. Code in subclasses can cooperate with code in superclasses via inheritance. Classes can have static methods and fields. Etc., etc.

To keep things simple here, we won't deal with any of these issues -- in fact, we won't even talk any more about objects or classes. (There is a lot of discussion in Pierce (2002)Benjamin C. Pierce (2002). “Types and Programming Languages”. MIT Press. ., if you are interested.) Instead, we'll study the core concepts behind the subclass / subinterface relation in the simplified setting of the STLC.

8.1.3. The Subsumption Rule🔗

τ₂ Our goal for this chapter is to add subtyping to the simply typed lambda-calculus (with some basic extensions). This involves two steps:

• Defining a binary subtype relation between types.

• Enriching the typing relation to take subtyping into account.

The second step is actually very simple. We add just a single rule to the typing relation: the so-called rule of subsumption:

                         Γ ⊢ t₁ ⦂ τ₁     τ₁ <: τ₂
                         --------------------------           (sub)
                               Γ ⊢ t₁ ⦂ τ₂

This rule says, intuitively, that it is OK to "forget" some of what we know about a term.

For example, we may know that t₁ is a record with two fields (e.g., τ₁ = {x:α→α, y:β→β}, but choose to forget about one of the fields (τ₂ = {y:β→β}) so that we can pass t₁ to a function that requires just a single-field record.

8.1.4. The Subtype Relation🔗

The first step -- the definition of the relation σ <: τ -- is where all the action is. Let's look at each of the clauses of its definition.

                              σ <: υ    υ <: τ
                              ----------------                        (trans)
                                   σ <: τ

                                   ------                              (refl)
                                   τ <: τ

                            σ₁ <: τ₁    σ₂ <: τ₂
                            --------------------                        (prod)
                             σ₁ × σ₂ <: τ₁ × τ₂

       f : C → Student
       g : (C→Person) → D

                                  σ₂ <: τ₂
                              ----------------                     (arrow_co)
                            σ₁ → σ₂ <: σ₁ → τ₂

                            τ₁ <: σ₁    σ₂ <: τ₂
                            --------------------                      (arrow)
                              σ₁ → σ₂ <: τ₁ → τ₂

       f : Person → C
       g : (Student → C) → D

    {name:String, age:Nat, gpa:Nat} <: {name:String, age:Nat}
    {name:String, age:Nat} <: {name:String}
    {name:String} <: {}

    {x:Student} <: {x:Person}

    {name:String,age:Nat} <: {age:Nat,name:String}

                        ∀ jk in j₁..jn,
                    ∃ ip in i₁..im, such that
                        jk=ip and σp <: τk
                  ----------------------------------                    (rcd)
                  {i₁:σ₁...im:σm} <: {j₁:τ₁...jn:τn}

                               n > m
                 ---------------------------------                 (rcdWidth)
                 {i₁:τ₁...in:τn} <: {i₁:τ₁...im:τm}

                       σ₁ <: τ₁  ...  σn <: τn
                  ----------------------------------               (rcdDepth)
                  {i₁:σ₁...in:σn} <: {i₁:τ₁...in:τn}

         {i₁:σ₁...in:σn} is a permutation of {j₁:τ₁...jn:τn}
         ---------------------------------------------------        (rcdPerm)
                  {i₁:σ₁...in:σn} <: {j₁:τ₁...jn:τn}

                            σ₁ <: τ₁    σ₂ <: τ₂
                            --------------------                (arrowWrong)
                            σ₁ → σ₂ <: τ₁ → τ₂

       f : Student → Nat
       g : (Person → Nat) → Nat

                                   --------                             (⊤)
                                   σ <: ⊤

                         Γ ⊢ t₁ ⦂ τ₁     τ₁ <: τ₂
                         --------------------------------            (sub)
                               Γ ⊢ t₁ ⦂ τ₂

                              σ <: υ    υ <: τ
                              ----------------                        (trans)
                                   σ <: τ

                                   ------                              (refl)
                                   τ <: τ

                                   --------                             (⊤)
                                   σ <: ⊤

                            σ₁ <: τ₁    σ₂ <: τ₂
                            --------------------                       (prod)
                             σ₁ × σ₂ <: τ₁ × τ₂

                            τ₁ <: σ₁    σ₂ <: τ₂
                            --------------------                      (arrow)
                            σ₁ → σ₂ <: τ₁ → τ₂

                               n > m
                 ---------------------------------                 (rcdWidth)
                 {i₁:τ₁...in:τn} <: {i₁:τ₁...im:τm}

                       σ₁ <: τ₁  ...  σn <: τn
                  ----------------------------------               (rcdDepth)
                  {i₁:σ₁...in:σn} <: {i₁:τ₁...in:τn}

         {i₁:σ₁...in:σn} is a permutation of {j₁:τ₁...jn:τn}
         ---------------------------------------------------        (rcdPerm)
                  {i₁:σ₁...in:σn} <: {j₁:τ₁...jn:τn}

8.1.5. Exercises🔗

The following "thought exercises" are repeated later as formal exercises.

      ∀ σ τ,
          σ <: τ  →
          σ→σ   <:  τ→τ
:::solution
      Answer: False
:::

      ∀ σ,
           σ <: υ→υ →
           ∃ τ,
              σ = τ→τ  ∧  τ <: υ

      ∀ σ τ₁ τ₂,
           (σ <: τ₁ → τ₂) →
           ∃ σ₁ σ₂,
              σ = σ₁ → σ₂  ∧  τ₁ <: σ₁  ∧  σ₂ <: τ₂

      ∃ σ, σ <: σ → σ

      ∀ σ τ₁ τ₂,
           σ <: τ₁×τ₂ →
           ∃ σ₁ σ₂,
              σ = σ₁×σ₂  ∧  σ₁ <: τ₁  ∧  σ₂ <: τ₂

    ∀ τ,
         ~(τ = Bool ∨ ∃ n, τ = A) →
         ∃ σ,
            σ <: τ  ∧  σ <> τ

  ∅ ⊢ (λp:τ×⊤. p.fst) ((λz:A,z). unit) ⦂ A→A

       ∅ ⊢ (λp:(A→A × B→B), p) ((λz:A.z), (λz:B.z)) ⦂ τ

       a:A ⊢ (λp:(A×τ). (p.snd) (p.fst)) (a. λz:A.z) ⦂ A

    a:A ⊢ (λp:(A×τ). (p.snd) (p.fst)) (a, λz:A. z) ⦂ A

       a:A ⊢ (λp:(A×τ). (p.snd) (p.fst)) (a, λz:A.z) ⦂ A

       ∃ σ,
         ∅ ⊢ (λp:(A*τ), (p.snd) (p.fst)) ⦂ σ

      exists σ t,
        ∅ ⊢ (\x:τ, x x) t ⦂ σ

      ∅ ⊢ (\x:⊤, x) ((λz:A,z) , (λz:B,z)) ⦂ τ

                            σ₁ <: τ₁    σ₂ <: τ₂
                            --------------------                        (prod)
                               σ₁*σ₂ <: τ₁*τ₂

                                   --------------
                                   τ₁*τ₂ <: τ₂*τ₁

8.2.1. Core Definitions🔗

8.2.2. Substitution🔗

The definition of substitution remains exactly the same as for the pure STLC.

8.2.3. Reduction🔗

Likewise the definitions of IsValue and Step.

8.2.4. Subtyping🔗

Now we come to the interesting part. We begin by defining the subtyping relation and developing some of its important technical properties.

The definition of subtyping is just what we sketched in the motivating discussion.

Note that we don't need any special rules for base types (Bool and Base): they are automatically subtypes of themselves (by refl) and ⊤ (by top), and that's all we want.

Note that, because the Subtype rules are not "syntax directed" (e.g., given a goal of the form ⊤ <: ⊤, you could apply the top rule, the refl rule, the trans rule), we have to use solve_by_elim here instead of apply_rules.

    Person := { name : String }
    Student := { name : String ; gpa : Float }
    Employee := { name : String ; ssn : Integer }

The following facts are mostly easy to prove in Lean. To get full benefit from the exercises, make sure you also understand how to prove them on paper!

8.2.5. Typing🔗

The only change to the typing relation is the addition of the rule of subsumption, sub.

We deliberately exclude HasType.sub from the list of constructors with the StlcSubTyping. apply_rules using StlcSubTyping will search for derivations without using the subtyping rule; if you want to make use of it in a derivation you will need to do so yourself.

Do the following exercises after you have added product types to the language. For each informal typing judgement, write it as a formal statement in Lean and prove it.

∅ ⊢ ((λz:A.z), (λz:B,z)) ⦂ (A→A × B→B)

∅ ⊢ (λx:(⊤ × B→B). snd x) ((λz:A. z), (λz:B. z)) ⦂ B→B

∅ ⊢ (λz:(C→C)→(⊤ × B→B). snd (z (λx:C.x))) (λz:C→C. ((λz:A. z), (λz:B. z))) ⦂ B→B

8.3.1. Inversion Lemmas for Subtyping🔗

Before we look at the properties of the typing relation, we need to establish a couple of critical structural properties of the subtype relation:

• Bool is the only subtype of Bool, and

• every subtype of an arrow type is itself an arrow type.

These are called inversion lemmas because they play a similar role in proofs as the inversion tactic: given a hypothesis that there exists a derivation of some subtyping statement σ <: τ and some constraints on the shape of σ and/or τ, each inversion lemma reasons about what this derivation must look like to tell us something further about the shapes of σ and τ and the existence of subtype relations between their parts.

There are additional inversion lemmas for the other types:

• Unit is the only subtype of Unit, and

• Base n is the only subtype of Base n, and

• ⊤ is the only supertype of ⊤.

When you do the products exercise, add your inversion lemma for products here:

8.3.2. Canonical Forms🔗

The proof of the progress theorem -- that a well-typed non-value can always take a step -- doesn't need to change too much: we just need one small refinement. When we're considering the case where the term in question is an application t₁ t₂ where both t₁ and t₂ are values, we need to know that t₁ has the form of a lambda-abstraction, so that we can apply the abs reduction rule. In the ordinary STLC, this is obvious: we know that t₁ has a function type τ₁₁→τ₁₂, and there is only one rule that can be used to give a function type to a value - rule abs - and the form of the conclusion of this rule forces t₁ to be an abstraction.

In the STLC with subtyping, this reasoning doesn't quite work because there's another rule that can be used to show that a value has a function type: subsumption. Fortunately, this possibility doesn't change things much: if the last rule used to show Γ ⊢ t₁ ⦂ τ₁₁→τ₁₂ is subsumption, then there is some sub-derivation whose subject is also t₁, and we can reason by induction until we finally bottom out at a use of abs.

This bit of reasoning is packaged up in the following lemma, which tells us the possible "canonical forms" (i.e., values) of function type.