Another Equivalent Structure

Loading...

Из курса от партнера University of Washington

Programming Languages, Part A

833 оценки

University of Washington

Programming Languages, Part A

833 оценки

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. 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. The three parts are not quite equal in length: Part A is almost as substantial as Part B and Part C combined. 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.

Из урока

Section 4 and Part-A Exam

We finish Part A of the course with this module. As explained in more detail in the welcome message, we discuss type inference, ML's module system, and the fundamental idea in computing of two computations being equivalent. There is no programming assignment -- instead there is an exam covering all of Part A. Finally, there is a brief wrap-up video for the end of Part A that also looks ahead to Part B and Part C -- we have put it after the exam, so don't overlook it.

Section Introduction1:45

What is Type Inference5:37

ML Type Inference6:09

Type Inference Examples10:27

Polymorphic Examples10:52

Optional: The Value Restriction and Other Type-Inference Challenges9:53

Mutual Recursion9:45

Modules for Namespace Management6:25

Signatures and Hiding Things7:02

A Module Example11:06

Signatures for Our Example11:03

Signature Matching4:03

An Equivalent Structure6:38

Another Equivalent Structure9:01

Different Modules Define Different Types3:32

Equivalent Functions8:41

Standard Equivalences10:01

Equivalence Versus Performance6:00

Познакомьтесь с преподавателями

Dan Grossman
Professor
Computer Science & Engineering

[MUSIC] In this segment, I'm going to show you a third

implementation of rational numbers that will be equivalent to our other two, as

long as we keep the type abstract. And what I'm going to do here, is

actually change the implementation of the type rational,

in order to emphasize that when the type is abstract, an equivalent structure can

go ahead and change how the type is implemented.

So, given a signature that has an abstract type, different structures can

have that signature while implementing the type in different ways.

Those structures might or might, might not be equivalent.

I'll show you an example where they are. So I'm about to show you a third

implementation, rational 3 And in rational 3, the type rational is going to

be implemented as a type synonym with int * int.

So let's go over and see that. Here is my structure.

You'll see I have a type synonym here, so in the rest of this module, rational and

int * int are the same type. The outside world, however, doesn't have

to know that. So before I show you these functions, how

about I just show you, remind you, what the three signatures look like?

Now signature RATIONAL_A requires the module to implement rational as this data

type. Since our module does not, rational 3

does not have this signature. If we try to give it this signature, the

type checker will reject it. But it does have this second signature,

RATIONAL_B. As we'll see, we already saw it defines a

type rational. It defines it to equal int * int. That's a fine way to implement a

type rational. But, given that definition, it's going to

have to have these three functions, where rational is int * int.

The outside world, as usual, will not know that rational is int * int,

and then for RATIONAL_C it can have this signature, provided it has everything it

had before, as well as a function of type int arrow rational.

And I'll show you that at the end. So, let's see how struct rational 3 is

implemented and the fact that it can have type, the signature RATIONAL_B.

So rationals are now just pairs of ints, in all cases.

So here's make_frac. If the denominator is 0, raise an

exception. If y less than 0, then produce (-x,-y).

Just like before, but now it's just a pair of ints, there's no frac constructor

involved. Otherwise return (x,y).

Notice we're not treating whole numbers any differently.

So if this denominator is 1, then we'll just, return (x,y).

Okay? To add 2 fractions, well, add needs to

take 2 rationals. And each rational is an int * int, so

this pattern will do well. And, we're not going to reduce things.

That's an orthogonal choice, but like Rational2, we're just going to wait until

toString to reduce things. So we'll just return a*d + c*b in the

first position, and b*d in the second position.

And then finally, toString is a little more complicated, because we still want

to return everything in reduced form and treat whole numbers specially here.

So here's what you need to do, if x is 0, you have a numerator of 0, you better

return the string 0. Otherwise We have some more work to do

here with GCD and reduce. so here's a let fun gcd equal this in,

let's convert to a string the numerator concatenated with if the denominator is

one then don't do anything. Else, a slash, and then to string of the

denominator. So, I didn't empahasize this.

Up here, I've computed the num and the denominator, by dividing both by the gcd,

of the absolute value of x and y. So, a bunch of arithmetic, but the point

is, to not print the denominator, if the, if the numerator is 0, or if the

denominator is 1. And so overall, if we go back up here to

the signature RATIONAL_B, we've provided everything at the right type,

make_frac returned an int * int, add took two int * ints and returned an

int * int. And toString took and int * int and

returned a string. And then the outside world does not know

that rational is int star int. Now, if we want to implement Rational3,

we also need a function, of type int arrow rational.

This was this cute thing where, for our other structures, the data type binding

was providing this function, and then we are exposing just that part of the data

type binding to the outside world. Now, in our new structure we don't have a

data type binding, we don't have such a function being defined by it,

but we can still implement this signature provided we have this function.

And so, again, it's a little cute, but down here at the bottom, I just defined a

function whole, you're allowed to start functions with a capital letter if you

want to, that just takes in an i and returns this

rational, this int * int of (i,1), and it works great.

So, that is our third implementation. I want to emphasize, that when we do

signature matching of this structure, against either RATIONAL_B or RATIONAL_C,

a couple of interesting things are going on.

So let me emphasize those for you. the first is make_frac internally has

type int * int arrow int * int. And so that does match a signature where

we're exploding, exporting it as int * int arrow rational, because rational is

int * int. And the client will never be able to tell

that we're actually returning something of the same type we're taking in, because

the client doesn't know those are the same types.

Now what's interesting, is we could If we went back here to RATIONAL_B, we could

say that make_frac, instead of being int*int arrow rational, it's actually

rational arrow rational. Now this is a very bad signature. The

structure has this signature. The type checker will accept it.

But, the structure will be useless. Because if all the outside world knows is

that it can use these bindings, it's never going to be able to call make_frac,

add or toString, because it can never get its first rational to get started.

There's no way it can call any of these functions.

So there are programs out there that type check and are not useful.

Okay? So we really want to expose here that make_frac does take 2 ints as

arguments. So that's the first interesting thing.

The second interesting thing is this function, whole.

So let me go back and show that to you here at the bottom.

Based on what we know from type inference, this is going to have type

alpha arrow alpha * int. And that is indeed what the type checker

will give this function internally, when it goes to type check it.

But in our signature in RATIONAL_C, we said this had to have type int arrow

rational. And so somehow, the type checker, which

is fairly sophisticated and fairly smart, has to get from this first type to this

second type legally, and it turns out it can, because the rules of signature

matching let you take a polymorphic function and instantiate it to a

non-polymorphic function. So the first thing the type checker has

to figure out to do, for signature matching, is to realize that alpha can be

int, and therefore, this could also have typed the less flexible type, int arrow

int * int. We have to replace all the alphas

consistently, and now we see, that indeed, since rational inside the module

is int * int, we can, as we usually do, match this type against this type in the

signature, and its pretty neat that ML does that for us.

Notice that this does not have something like the type, alpha arrow int * int, or

you know, int arrow alpha * int. When you take a generic type, a

polymorphic type and make it less general, you have to replace all the

alphas with another type. The, this function hold does not have

these bottom two types, that doesn't make any sense.

It is not the case, that if you called whole with a string, you would get back

an int * int, so these types are just wrong and I will delete them.

It is interesting to me that inside this module, we actually could call whole with

a string for i, but outside the module, because of what the signature says, we

can only call it with an int, and therefore it will return irrational.

Okay? So, that is the more sophisticated and interesting details of this third

structure. But the high level point is that under

RATIONAL_B or RATIONAL_C, this structure is equivalent to our other two

structures, even though it implements the type

rational and in, and in an entirely different way.

Ознакомьтесь с нашим каталогом

Присоединяйтесь бесплатно и получайте персонализированные рекомендации, обновления и предложения.

Coursera делает лучшее в мире образование доступным каждому, предлагая онлайн-курсы от ведущих университетов и организаций.

© Coursera Inc., 2018 Все права защищены.

Загрузить из App Store

Загрузить в Google Play