[As described below, this is Part C of a 3-part course. Participants should complete Parts A and B first -- Part C "dives right in" and refers often to material from Part A and Part B.] This course is an introduction to the basic concepts of programming languages, with a strong emphasis on functional programming. The course uses the languages ML, Racket, and Ruby as vehicles for teaching the concepts, but the real intent is to teach enough about how any language “fits together” to make you more effective programming in any language -- and in learning new ones. This course is neither particularly theoretical nor just about programming specifics -- it will give you a framework for understanding how to use language constructs effectively and how to design correct and elegant programs. By using different languages, you will learn to think more deeply than in terms of the particular syntax of one language. The emphasis on functional programming is essential for learning how to write robust, reusable, composable, and elegant programs. Indeed, many of the most important ideas in modern languages have their roots in functional programming. Get ready to learn a fresh and beautiful way to look at software and how to have fun building it. The course assumes some prior experience with programming, as described in more detail in the first module of Part A. Part B assumes successful completion of Part A. The course is divided into three Coursera courses: Part A, Part B, and Part C. As explained in more detail in the first module of Part A, the overall course is a substantial amount of challenging material, so the three-part format provides two intermediate milestones and opportunities for a pause before continuing. The three parts are designed to be completed in order and set up to motivate you to continue through to the end of Part C. Week 1 of Part A has a more detailed list of topics for all three parts of the course, but it is expected that most course participants will not (yet!) know what all these topics mean.
Function Subtyping
Loading...
来自 University of Washington 的课程
Programming Languages, Part C
257 个评分
从本节课中
Section 10, Final Exam, and Course Wrap-Up
We have reached the last module of Programming Languages! We first study subtyping, how it relates to static types for object-oriented programming, and how it relates to generics. There is no assignment or quiz devoted only to this last "new material", but there is a "final exam" covering Part B and Part C of the course. Enjoy studying for the exam, and don't miss the final "wrap-up" lesson when you're all done!
与讲师见面
Dan GrossmanProfessor
Computer Science & Engineering
[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.
