[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. So the first thing is what we've been talking about. This has a name, it's called width subtyping, that you can take a wider record and make it a subtype of a slimmer record, provided that that slimmer record has all field names and types that are in the wider record. So that's the rule we have been talking about, and you can do that. Basically, you can take your wider record and drop some of the fields. Fine, here's another rule that maybe it didn't even occur to you we might need. How about I have two records that have the same fields and the same types, but they're not written down in the same order? Well the order doesn't matter, right? When I'm writing down a record type, it doesn't matter if I say x colon real y colon real, or if I say y colon real x colon real. So we should let one record type be a sub type of another record type that just permutes the order of the fields. It doesn't change the types of the fields, it doesn't change what fields are there, but writes them out in a different order. And that's a very nice rule. It seems to clearly pass our substitutability test. Because we'll still be able to get and set all the same fields. My point is if you don't write this down as part of your subtyping relation, all sorts of programs don't type check that you really want to type check. So it's a great rule to put in your subtyping relation. And then we have two that kind of come along for free, that every sub typing relation should have. But we should be explicit about them. The first one is transitivity, that if t1 is a sub type of t2, and t2 is a subtype of t3, then t1 is a sub type of t3. This should follow directly from substitutability. If a value of t1 can be used as a value of t2, and a value of t2 can be used as a value of t3, then a value of t1 should be usable as a value of t3. This is a nice rule to have because that way our other rules, our rules that actually do something more interesting, don't have to say everything all at once. That if we want to think of subtyping as dropping a field and then re-ordering fields, width, and then permutation, we can use transitivity to get it to work that way. And finally, one you might think is really weird. It's called reflexivity, it's a word from discreet matthematics or logic. Every type is a subtype of itself. So t is a subtype of t for any type t. And we don't really need that so far, but when we see some other subtyping rules, in particular the subtyping rules for functions, which we'll get to shortly, it'll be nice to have this rule because it helps simplify other rules in ways that we'll see. So summary, we have one new typing rule. If t1 is a sub type of t2 and e has type t1, then e also has type t2. And then we have to define the notion of two subtypes being subtypes of each other. And this slide is where we made our preliminary definition. These rules are all fine. And in upcoming segments, we'll try to add additional rules. And see if we can do that in a sound way.
