[MUSIC] This segment has perhaps the most counterintuitive result in the entire course. It's also exactly the sort of things that you take a programming language course to learn. So we're going to discuss subtyping for functions, and let me be clear about what I mean here. Now, there's some things we already know. We know if you're the caller to a function, you can pass a subtype of the argument that the function is already expecting. And similarly, after you get back something from the function, like maybe you get back a color point, you can think of that color point as a point. This is all normal subtyping. Doesn't matter that we're using it with a calling a function. More interesting is to ask the question when is one function itself having a type that is a subtype of another function type and this is important in a language with high order functions. Suppose the function argument is itself a function, something of type t1 arrow t2 using our ML syntax for function types. Takes a t1 and returns a t2. If that's the argument to some other function, are you allowed to pass in a t3 arrow t4 instead, and under what circumstances? Clearly, t1 arrow t2 and t3 arrow t4 are going to have to be related somehow. You can't just pass in some totally different function with some totally different type. But is there a subtyping relationship there? And let's try to figure out what it is. This is not just important for subtyping and languages with higher order functions. What we're going to study here is also directly relevant to subtyping for object oriented languages and we'll study that next. It's just a little easier to understand in my opinion, thinking about functions first. So here's an example we're going to build off of. There's actually no subtyping on this slide but I just want to show you a higher order function involving records. So it's a function distMoved. It takes in a function f and a point p, it calls f with p and then it returns the distance between p and f of p. All right? That's all it does. It's a little function. So f has type x:real, y:real, arrow x:real, y:real. It takes a point and returns a point. P is a point. And then the body here calls f with p, determines how much the x coordinate changed, determine how much the y coordinate change and returns the appropriate distance. Here's a completely normal call to it. Here's a function flip that takes a point and negates the x coordinate and the y coordinate to produce a new point. So it's a functional, flip it around on both axes, and then we called distMoved with the function flip and some point, like x coordinate's 3, y coordinate is 4. There's no subtyping here yet, because flip has type (x:real, y:real) arrow (x:real, y:real), which is exactly the type that distMoved expects. Okay, so this works fine. Now let's consider this call. It's exactly the same definition of distMoved. But now I want to pass in this function flipGreen. What it does is it to builds a new record, that flips x, flips y and adds a color field green. Okay? So the return-type of flipGreen is {x:real, y:real, color:string}, so flipGreen overall takes an {x:real, y:real} and returns an {x:real, y:real, color:string}. distMoved does not expect exactly that type. It expects an {x:real, y:real} arrow (x:real, y:real). But it's no problem if we add this subtyping rule. That if ta is a subtype of tb, then t arrow ta is a subtype of t arrow tb. In other words, we're allowed to go into the return type of a function. And add subtyping there. So a function is allowed to return something with fields we don't need, something extra. A function can return more than it needs to. There's jargon for this. We say that function types are covariant in their return type. I will not test you on that jargon, but if you've ever heard the term covariance they mean the subtyping goes the same way, and here the subtyping goes the same way of ta is a subtype of tb then arrow ta is a subtype of arrow tb. So that works great for the return type. But, what about the argument type? So here's a different function we're trying to pass in to distMoved. FlipIfGreen says if p's color is green then build this record with an x field and a y field. Otherwise build this other record with an x field and a y field. Now the argument type of flipIfGreen is x:real,y:real,color:string. Excuse me. It requires all three fields. But up here in distMoved, we pass to the function something that does not have a color field. If you look at this call, we call distMoved with flipIfGreen and something that just has an x field and y field. This will get stuck. This if you try to run this program, it's not sound. It will try to read the color field of a record that does not have a color field. And therefore, we better make sure this code does not type-check. And so what we cannot allow is subtying on argument types. Just because ta is a subtype of tb you cannot allow ta arrow t to be a subtype of tb arrow t. You cannot say, it's okay to assume this function doesn't need all the fields. It does need all the fields. Or at least it might. And so you cannot drop fields from arguments to functions. So this better not type check. We better not have this type checking rule. What may surprise you is it's okay to go the other way. It's okay to allow subtyping on function argument types as long as that subtyping is backwards, as long as it goes the other way. You see the rule here in this last bullet at the bottom. It turns out that if tb is a subtype of ta then ta arrow tt is a subtype of tb arrow t. See how I flipped it around? The subtype here is in the super type of the result. Okay? So this has a jargon its called contravarience but what it's saying is a function can assume less than it needs to about arguments. So here's your example. It turns out it's fine to call distMoved with a function that does not need an x:real and a y:real. Maybe it only needs an x:real. Here's an example. This function flipX Y0 takes in a point, returns, takes in some p. Returns a new record that has an x field that's minus p.x and the y field, it's just zero. So notice it never asked for p.y, it does not care if p has a y field. So if I pass flipX_Y0 in to distMoved, distMoved needs f to work as though it had this type. In flip X_Y0 can act like it has that type even though it does not need its argument to have a y field. So, flipX_Y0 has an argument type of x:real, but we can pretend it has an argument type of x:real, y:real. Yet x:real, y:real is the subtype compared to x:real, and that's why this subtyping rule is reversed. This is the correct rule that says if tb is less than ta then ta arrow t is less than tb arrow t. And it turns out you could do both at once. So, here's our final example, flipXMakeGreen returns a record with an x field, a y field and a color field and only requires its argument to have an x field. So we can pass this in for distMoved, flipXMakeGreen has type, if you give me an x:real, I'll give you back an x:real, y:real, color:string. If you just look at flipXMakeGreen, that's the type it should have. We can pass it into distMoved, which expects an x:real, y:real arrow, x:real, y:real. And nothing bad will happen, because this function works just fine if you give it something with an x field and a y field. And it always gives back something that has an x field and a y field. It just happens to give back more, and it happens to need less. We're just combining the two ideas together. And that's why the general rule for function subtyping is that if t3 is a subtype of t1 and t2 is a subtype of t4, then t1 arrow t2 is a subtype of t3 arrow t4. And so we see for the result types, t2 and t4, the subtyping goes the same way and for the argument types, t3 and t1, it's flipped around and it goes the other way. So the fancy jargon way of saying this is that function subtyping is contravariant in its arguments and covariant in its results. And this is essential for understanding subtyping and object oriented programming, actually, and understanding how it is sound to override methods in a subclass in a language with subtyping and we'll see that next. I would just like to be honest as I said at the beginning that I think this is the most unintuitive concept in the course. When you get confused, I can encourage you to go back and work through the examples or make up your own examples and convince yourself that the arguments really are contravariant, they really do have to be flipped around. Otherwise you can break the soundness of the type system. Now many smart people have gotten this wrong, have made mistakes about this and I just want to emphasize this point; that some point in your life you may make this mistake, your boss might make this mistake, your friend might make this mistake and so I'm trying to just get you to memorize that there's something weird going on here and you can always come back and watch this video later. And if nothing else, I want you to know that I do have a PhD programming languages and I am happy to jump up and down and insist that subtyping for functions and methods has to be contravariant in the arguments. I'm going to do this quite literally, because I think it's silly and I think it's fun and you might remember it that way. So here's what I'm going to do. Actually, I moved the chair to the side. I'm actually jumping up and down and while I'm jumping up and down I'm telling you that function subtyping has to be contravariant in the arguments and it's not the direction that you usually think it is. And with that, we can conclude our study of function subtyping.
