8.1.4.1. Structural Rules🔗

To start off, we impose two "structural rules" that are independent of any particular type constructor: a rule of transitivity, which says intuitively that, if σ is better (richer, safer) than υ and υ is better than τ, then σ is better than τ...

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

... and a rule of reflexivity, since certainly any type τ is as good as itself:

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

8.1.4.2. Products🔗

Now we consider the individual type constructors, one by one, beginning with product types. We consider one pair to be a subtype of another if each of its components is.

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

Suppose we have functions f and g with these types:

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

Is it safe to allow the application g f?

Yes.

So we want:

      C→Student  <:  C→Person

I.e., arrow is covariant in its right-hand argument.

Now suppose we have:

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

Is it safe to allow the application g f?

Again yes.

So we want:

      Person → C  <:  Student → C

I.e., arrow is contravariant in its left-hand argument.

Putting these together...

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

8.1.4.3. Records🔗

What about subtyping for record types?

The basic intuition is that it is always safe to use a "bigger" record in place of a "smaller" one. That is, given a record type, adding extra fields will always result in a subtype. If some code is expecting a record with fields x and y, it is perfectly safe for it to receive a record with fields x, y, and z; the z field will simply be ignored. For example,

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

This is known as "width subtyping" for records.

We can also create a subtype of a record type by replacing the type of one of its fields with a subtype. If some code is expecting a record with a field x of type τ, it will be happy with a record having a field x of type σ as long as σ is a subtype of τ. For example,

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

This is known as "depth subtyping".

Finally, although the fields of a record type are written in a particular order, the order does not really matter. For example,

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

This is known as "permutation subtyping".

We could formalize these requirements in a single subtyping rule for records as follows:

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

That is, the record on the left should have all the field labels of the one on the right (and possibly more), while the types of the common fields should be in the subtype relation.

However, this rule is rather heavy and hard to read, so it is often decomposed into three simpler rules, which can be combined using trans to achieve all the same effects.

First, adding fields to the end of a record type gives a subtype:

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

We can use rcdWidth to drop later fields of a multi-field record while keeping earlier fields, showing for example that {age:Nat,name:String} <: {age:Nat}.

Second, subtyping can be applied inside the components of a compound record type:

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

For example, we can use rcdDepth and rcdWidth together to show that {y:Student, x:Nat} <: {y:Person}.

Third, subtyping can reorder fields. For example, we want {name:String, gpa:Nat, age:Nat} <: Person, but we haven't quite achieved this yet: using just rcdDepth and rcdWidth we can only drop fields from the end of a record type. So we add:

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

It is worth noting that full-blown language designs may choose not to adopt all of these subtyping rules. For example, in Java:

• Each class member (field or method) can be assigned a single index, adding new indices "on the right" as more members are added in subclasses (i.e., no permutation for classes).

• A class may implement multiple interfaces -- so-called "multiple inheritance" of interfaces (i.e., permutation is allowed for interfaces).

• In early versions of Java, a subclass could not change the argument or result types of a method of its superclass (i.e., no depth subtyping or no arrow subtyping, depending how you look at it).

8.1.4.4. ⊤🔗

Finally, it is convenient to give the subtype relation a maximum element -- a type that lies above every other type and is inhabited by all (well-typed) values. We do this by adding to the language one new type constant, called ⊤ (pronounced "⊤" and written ⊤), together with a subtyping rule that places it above every other type in the subtype relation:

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

The ⊤ type is an analog of the Object type in Java and C#.

8.1.4.5. Summary🔗

In summary, we form the STLC with subtyping by starting with the pure STLC (over some set of base types) and then...

• adding a base type ⊤,

• adding the rule of subsumption

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

to the typing relation, and

• defining a subtype relation as follows:

                              σ <: υ    υ <: τ
                              ----------------                        (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.2.1.1. Syntax🔗

Omitting records, to avoid dealing with "..." stuff.

Checks that the extended grammar parses the way it should.