[MUSIC].
In this segment we're going to give a very precise definition to subtyping and
do it in a way that we can add a lot more flexibility to our type system without
having to change any of the typing rules we already had in our programming language
or have learned earlier in the course.
So this is important because a programming language
already has a lot of typing rules.
And they're complicated and sophisticated, and if we had to make
complicated changes to all of them just to support a passing a record
with three fields where we only needed two of those fields, that would be annoying.
We have great typing rules.
For example, when you pass an argument to a function,
the type of that argument should equal the type of the function parameter.
It's a nice rule, it's easy to explain.
We can implement it in our language, but that rule in and
of itself is what in the previous segment did not let us pass something
that we wanted to pass and that would do no harm.
So the way we're going to fix this now is by adding just two things to our language.
The first thing we're going to add is a notion of subtyping,
separate from everything else.
So, on the slides, I'm going to write t1 <: t2, to mean t1 is a subtype of t2.
This does not have to be syntax in your language.
This is just a binary relation on two types.
Given two types, t1 and t2, maybe one is a sub type of the other and
maybe they're not.
And what we're going to have to do is come up with a definition of that relation.
Just like the less than relation on integers is a binary relation,
takes two integers and either the left one is less than the right one or it's not.
We are going to define a relation on two types.
Now once we have that relation, which we call the subtyping relation,
now all we do to our programming language is we add exactly one rule.
And it's the rule you see in blue here.
It says if some expression has type t1, and
if t1 is a subtype of t2, then e also has type t2.
And that's the only rule we have to add and everything will just work out.
For example If x colon real y colon real color colon string
is a subtype of x colon real y colon real,
then anything of the type with three fields also has the type with two fields.
And since it also has that type,
we'll be able to pass it to a function that expects the super type.
So we've really separated things out very, very nicely here.
Now we do want to do this carefully.
There's a common misconception by people who don't actually
work on programming languages, that if you're making up a new language,
you can do whatever you want because it's your language.
And as we've learned repeatedly in the course,
yes you have a lot of flexibility in language design, but if you do it wrong,
your language doesn't work the way you expect.
For example, dynamic scoping for closures is a terrible idea for lots of reasons.
The same thing is true with typing and subtyping rules.
That you can't just use whatever rules you want,
at least not if you want your type system to actually accomplish something, right?
Back when we learned about static typing,
we learned that the purpose of a type system is to prevent certain operations.
In the language, we’re studying for subtyping the purpose is to
make it impossible to ever have a program that type checks, but
when you run it, you try to access a field of a record that is not in that record.
So it turns out that with just our typing rules from the previous segment,
we have that property.
We are sound for preventing the bad record field accesses.
Now, when we add subtyping, we want to make sure we stay sound.
If we define the subtyping relationship in a way that ruins the soundness of our
type system, I would say we've done the wrong thing.
And there's a little saying about this in programming languages which is that
sub typing is not a matter of opinion, right,
either your sub typing rules break your soundness, or they don't.
It's important to us that they not break the soundness.
So the key thing you have to reason about for
not breaking it [COUGH] is this idea of substitutability.
So if t1 is a sub type of t2, then what we want is that any
value of type t1 can be used in every way a value of t2 can be.
So, this is going to be true for our example with a record with more fields.
In the super type where we just have x colon real y colon real,
the only thing you can really do with that record besides pass it around
is get the x field, get the y field, set the x field, set the y field.
And you can do all of those things with something of
type x colon real y colon real color colon string.
So the substitutability principle holds, all right?
So that's why this works, and
that's why that's a legitimate thing to add to our subtyping relation.
So, without further ado, how about I add,
I now define at least a preliminary subtyping relation.
These are all things that I'm going to use to say that one type t1
can be less than another type t2.