[MUSIC] This is the first of several segments where we will study subtyping, which we've mentioned only briefly so far when considering interfaces. And I want to do this to build up the key ideas from first principles. This will be the last major topic of the course, and I think it really finishes our foundation of the main ideas that we use to create programming languages. I'm going to do this all in pseudocode. You're only going to see PowerPoint slides because we don't have time for another programming language. And even if we did real programming languages always handles subtyping in a more complicated way than the core ideas underneath whats in actual languages. So I'm going to show just subtyping first, then after we understand subtyping, using just PowerPoint then we can relate it back to some important questions, like how statically typed object oriented programming languages use subtyping? How subtyping relates to the generic sim polymorphism we saw on ML? How they have complementary strength and in fact, at the very end, how you can combine them to get something that's actually greater than the sum of the parts. So, we're going to start from the beginning, we'll get all to that later. And what we're going to do is cover most of the ideas by just imagining a small language that will have functions, and addition, and arithmetic, and all that. But the key thing it is going to have is records. Those were those things in ML that had fields and contents. They're a lot like objects, if objects only had instance variables but not methods. But we're going to make those fields mutable. Okay, so a record is something with mutable fields. You can get the fields, you can set the fields. We'll make up our only syntax because none of the languages we have studied would be appropriate. ML has records, so our syntax will be most like ML, but it doesn't have subtyping, so I would confuse you if I used actual ML. And it does not have mutable fields. Fields are immutable in ML. Racket and Ruby are dynamically typed languages, and this is all about static typing, so that would be weird. And even if we all know Java which we don't, it uses class names this types and I don't want to do that for understanding what subtyping is really about. So, I have to take a little bit here to just explain to you my language, okay? So, here are records in my language. There are three constructs related to record the first one creates records. So this one actually does look just ML, you write curly braces, write a field name, equal and expression is separate those by commas. So the F0 is just names of fields, like full bar X whatever and the Es are expressions. and the semantics of this syntax is a value at each of the expressions to values then return a record value that has all of these fields holding the contents of the results of the expressions. Okay. That is exactly like an amount. The second concert we have is field access. So if you write e.f what that means is evaluate e to a value v. Assuming that it's a record that has an f field, retrieve the contents of that field. Otherwise, it would be an error. But in fact, our type system is going to make sure that that never happens. That e in fact if type checking succeeds is always a record that has an f field, so, e.f just retrieves the contents of that field. In ML we actually wrote this #f e, but e.f is much more common in programming languages. It looks more like a Ruby getter, so I'll write e.f. Lastly we have record field update, here we write e1.f=e2, we evaluate e1 toa record within f field just like we did in accessing, but now we update the contents of that field to be the result of evaluating e2, so the semantics are. Evaluate e1 and e2 to values. e1 should be a record with an f field. Update, mutate its f field to hold e2. So that is our syntax and our operational semantics for records. because we're setting typing, we also have typing rules. So, it turns out, we have a special kind of type for records. And this also just looks like in ML. So we write curly braces, field names, colons, and the types. So this record type says this describes records that have a field f1 holding type t1, a field f2 holding type t2, up to a field fn holding type tn. So every record in our language will have some type that looks like this if it has an x that holds an int, and y that holds a string then the record type would be x colon int, y colon string. Now that we have these types, we can use them to have type checking rules for the three kinds of expressions I showed you on the previous slide. Let's do each of them in order. So the way you type check a record creation function is you give it a record type that has all the same field names and field 1 has type t1 if e1 has type t. And field 2 has type t2 if e2 has type t2 and so on. That much is again, like an ML. For accessing the contents of a field, if e has a record type, containing a field f that has type t, then e.f has type t, right? So e has some record type, that record type tells you the type of the f field, that is the type of the record access expression e.f. If there is no f field in the type of e, then this shouldn't type check. And that's exactly how the type-checker prevents reading fields that are not in records, which would be a runtime error. We're going to prevent those errors with our type system. And finally, record update works basically the same way. The way you type check e1.f = e2, you make sure that e1 has a record type that includes an f field. And whatever the type of that f field is, e2 better have that type. So that when you update the contents, the records still has the same okay, so those are our typing rules. So let's put it together with a small example that will mostly look like ML, but this is really pseudocode, right? You couldn't type this in because it uses this dot notation, which is not ML, okay? So here's a little program where a function distToOrigin takes in a point as an argument so, we're not doing anything OP here, this is no method call, this is a function. It takes in an argument p, and that argument has dev type x:real, y:real, a point within x coordinate and a y coordinate. And the body of this function returns the square root of p.x*p.x+p.y*p.y, so we get the contents of the x field, of p we get it again. We multiply those together, we get the y fields twice and so on. So we could use this function by calling it distToOrigin with some argument like pythag which is a variable of type x:real, y:real. And it could have that type because this record expression x=3.0, y=4.0 would have type x:real, y:real. So this all works, you make the call the distToOrigin, distToOrigin returns something of type real because that's the return type of math.sqrt, and we presumably get a value like 5.0 because the square root of three squared plus four squared is five. So, this is using our language and this should all type checked. We haven't seen any subtyping it, we're finally ready to motivate some subtype. Let's look at the slightly different example, in this code example, it's exactly like what I had before except this. I'm calling dist to origin with c Where c is this color point that has x:real, y:real, and color:string. And so you can have that type, because the record that it is bound to has an x field that holds a real, a y field that holds a real, and a color field that holds a string. But now in the languages I have described it so far, this function call should not type check because when you have a function that expects an argument of a certain type, you have to pass an argument of that type. And dstToOrigin expects an x:real,y:real and c is an x:real,y:real,color:string. If they are not the same type the function called doesn't type check but, we would like this to type check. There is nothing wrong going on here, c just has a type that has some more fields, some extra fields, it's not going to bother dist to origin if there's a color field. So, we would like to make a tight system more flexible such that this function called type checks just like you see here on the slide and that's a good idea, and the easiest way to that is to add subtyping into your language. So this is a fairly natural idea, which is that if you have some record type, so some expression in your language has some record type with some fields, f1 of type t1, f2 of type t2, up to fn of type tn, then let's let it also have that type with some of the fields removed. So if you have an x:real, y:real color:string. Let that also have type x:real, y:real and that's what we need to make code like this type-checked. I have a different example here to emphasize that we, with this rule it's not just that we can take c and call distToOrigin with it, like I wanted to on the previous slide. We could also call another function that just requires its argument to have type color:string, a record that only has one field color. In that case it's fine that it also has an x field and a y field. And maybe makePurple updates the record so that its color field is now purple. It'd be perfectly fine to pass c to that function. And then, after we called it, c would not be a green point any more. It would be a purple point. So if we want these things to type-check, we need a type system that allows this sort of you can forget fields. And as we'll see in the next segment subtyping is a very elegant way to add this kind of flexibility to your type system.
