Understanding Subtyping in Programming Language Theory: A Step-by-Step Proof

this lecture is from CSCE-550, Nov 12, 2024.

The Why?

Why understand the lecture on Programming language theory (Subtyping) is important to study ?

Today's lecture highlighted the significance of programming language theory, particularly in the context of type systems. This theory is crucial for:

• Creating Flexible and Safe Type Systems: Designing type systems that balance flexibility and safety.
• Understanding Type Substitutability: Knowing when one type can be safely used in place of another.
• Implementing Inheritance: Supporting features like inheritance in object-oriented languages.
• Early Error Detection: Enabling type checkers to catch errors before runtime while maintaining practical usability.

interface Person {
 name: string;
 age: number;
}

interface Employee {
 name: string;
 age: number;
 salary: number;
}

let person: Person;
let employee: Employee = {name: "Alice", age: 30, salary: 50000};
person = employee; // This works! Thanks to width subtyping

First thing first let's note:

<: means subtype?

Yes, exactly!

A <: B means A is a subtype of B or A is more specific than B or A can be safely used wherever B is expected

1. Some examples:
2. Dog <: Animal (a Dog is a type of Animal)
3. {x,y,z} <: {x,y} (a record with x,y,z is a subtype of a record with just x,y)
4. Integer <: Number (an Integer is a type of Number)

Subtyping Rules:

1. S-Refl (Reflexivity):
2. Every type is a subtype of itself
3. Like how Int is a subtype of Int
4. A = A
5. S-Width (Width subtyping):
6. A type with more fields is a subtype of a type with fewer fields
7. Like how a Person{name, age, email} can be used wherever a Person{name, age} is expected
8. You can always forget extra information safely
9. S-Trans (Transitivity):
10. If A is a subtype of B, and B is a subtype of C, then A is a subtype of C
11. If Student <: Person and Person <: Mammal, then Student <: Mammal
12. Helps us chain relationships together
13. S-Depth (Depth subtyping):
14. If a field's type is a subtype, the whole record is a subtype
15. If we know a Dog is a kind of Animal (Dog <: Animal)
16. Then a "record/struct/object that has a pet Dog" should be usable wherever we expect a "record/struct/object that has a pet Animal"
17. Allows subtyping to work on nested structures
18. S-Perm (Permutation):
19. The order of fields doesn't matter for record types
20. Order shouldn't matter in record types

{name: String, age: Int} 
is the same as
{age: Int, name: String}

This json works because the type system understands these subtyping relationships. The theory we're looking at explains why this is safe and how to prove it formally.

Proving Subtyping Relationships:

What we want to prove?

{y:Nat, x:{a:Nat,b:Nat}} <: {x:{a:Nat}}

// Complex type (left side of <:)
{
  y: 42,          // has a y field that's a number
  x: {           // has an x field that's a record
    a: 1,         // with an a field that's a number
    b: 2         // and a b field that's a number
  }
}

// Simple type (right side of <:)
{
  x: {           // only needs an x field that's a record
    a: 1         // with just an a field that's a number
  }
}

// Simple interface - what a function might expect
interface SimpleType {
    x: {
        a: number
    }
}


// A function that only cares about x.a
function printA(obj: SimpleType) {
    console.log(obj.x.a);
}


// Our complex type with extra stuff
const complexObj = {
    y: 42,
    x: {
        a: 1,
        b: 2
    }
}


// This should work fine! Even though complexObj has extra fields
printA(complexObj);  // prints: 1

We're trying to prove the complex record can be used wherever the simple record is expected. But this is a big leap to prove directly!

So we pick a middle ground - T2:

// T2 (our intermediate step)
{
    y: 42,                    // still has the y field
    x: {                      // has the x field
        a: 1                  // but x only has a, dropped b
    }
}

let me explain T2 with a simpler analogy!

Think of it like proving a friend can get from New York to Los Angeles:

1. Full journey: New York → Los Angeles (hard to prove in one step!)
2. So we break it into:

• New York → Chicago
• Chicago → Los Angeles

Chicago is like our T2 - it's a stepping stone or midpoint that makes the proof easier.

In our type problem:

Start: {y:Nat, x:{a:Nat,b:Nat}} // Like New York
T2:  {y:Nat, x:{a:Nat}}    // Like Chicago (our midpoint!)
End:  {x:{a:Nat}}        // Like Los Angeles

We need to prove:
1. Start → T2   (Drop b)
2. T2 → End    (Drop y)

T2 is just a midpoint type we invented to make the proof easier. Instead of making one big jump (proving Start can be used as End directly), we prove:

1. First we start, then we drop b:Nat from our new york, to come to T2 i.e Chicago
2. We pick T2 then we drop y again making it End expresssion i.e {x:{a:Nat}}

We don't drop both at once! That's the whole point of having T2 - it lets us drop one thing at a time, making each step simpler to prove. It's like:

• First prove we can safely drop b
• Then separately prove we can safely drop y

R1: The original problem we need to prove:

{y:Nat, x:{a:Nat,b:Nat}} <: {x:{a:Nat}}

This is our end goal!

R2: First step with T2:

{y:Nat, x:{a:Nat,b:Nat}} <: T2

where T2 = {y:Nat, x:{a:Nat}}, This shows we can drop the b field.

After dropping b, we have T2 = {y:Nat, x:{a:Nat}} and we want to get to {x:{a:Nat}}

But we don't just drop y directly.

R3: States that T2 can become our final form

{y:Nat, x:{a:Nat}} <: {x:{a:Nat}}

let's hold on R3 at the moment, we will come back to R3 after R4 & R5

R4 & R5 together PROVE R3 is true by:

So R3 is like saying we can do this and R4+R5 show here's how we do it!

Now with THIS RESULT, R1 & R2 we do R4:

R4 (Permutation Rule - S-Perm):

{y:Nat, x:{a:Nat}} <: {x:{a:Nat}, y:Nat}

This just says we can reorder fields:

1. Left side has "y then x"
2. Right side has "x then y"
3. They're the same thing, just reordered!

Applying S-Width rule (R4):

The S-Width rule says we can drop fields from a record type, but in many type systems, we want this to be predictable and mechanical. So the convention is that we can drop fields from the end or right side of the record.

for example:
// We can drop the last field using S-Width
{x:Nat, y:Nat, z:Nat} <: {x:Nat, y:Nat} // OK-dropping from end
{x:Nat, y:Nat} <: {x:Nat}         // OK - dropping from end

// But we can't directly drop from middle
{x:Nat, y:Nat, z:Nat} <: {x:Nat, z:Nat} // NOT OK-can't drop y from middle

that's why we needed step R4 (permutation) first:

1. R4: Move y to the end: {y:Nat, x:{a:Nat}} <: {x:{a:Nat}, y:Nat}
2. R5: Now that y is at the end, we can drop it: {x:{a:Nat}, y:Nat} <: {x:{a:Nat}}

It's like:

1. First use S-Perm to get the field you want to drop to the end
2. Then use S-Width to drop it

R5 (Width Rule - S-Width):

{x:{a:Nat}, y:Nat}  <:  {x:{a:Nat}}

Conclusion

Thus, using valid subtyping rules, we have shown that

{y: Nat, x: {a: Nat, b: Nat}} <: {x: {a: Nat}}

This is proven by:

1. Dropping the Inner Field (R2): First, we eliminate the b field from the record.
2. Reordering Fields (R4): Next, we reorder the fields to position y at the end.
3. Dropping y: Finally, we remove the y field, completing the proof.

This proves our original sub typing relationship is valid!

Each step used only our allowed rules (S-Width, S-Perm, S-Depth, etc.) to get from start to finish.

This demonstrates how we can derive valid conclusions through a series of logical steps.