[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.
The Subtype Relation
Loading...
來自 University of Washington 的課程
Programming Languages, Part C
211 個評分
從本節課中
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].
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.
