Explore
For Enterprise
Join for Free
Log In

艺术与人文
商务
计算机科学
数据科学
信息技术
健康
数学和逻辑
个人发展
物理科学与工程
社会科学
语言学习
学位
证书

浏览 Coursera 的全部课程

浏览
搜索
企业版
登录
免费加入

What is Static Checking?

Loading...

Programming Languages, Part B

华盛顿大学

4.9（448 个评分） | 12K 名学生已注册

[As described below, this is Part B of a 3-part course. Participants should complete Part A first -- Part B "dives right in" and refers often to material from Part A.] 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.

查看授课大纲

您将学习的技能

Racket (Programming Language), Programming Language Concepts, Type System, Functional Programming

审阅

4.9（448 个评分）

5 stars
419 ratings
4 stars
27 ratings
3 stars
2 ratings

KR

Mar 23, 2018

I'm a pretty experienced C/C++ programmer and this course has been a brilliant introduction into functional programming and the underlying philosophies underpinning programming languages in general.

JM

May 09, 2018

DO THIS COURSE. It brings together everything in part A. In particular, the final shorter week on the differences between Statically and dynamically typed languages is mind-bending and brilliant.

从本节课中

Section 7 Including a Quiz

In the last module of Part B we will use our experience programming in ML and Racket to compare and contrast static typing and dynamic typing. This is not only the most important difference between these two languages, but it is a fundamental topic in the study of programming languages. Learning it can help you program more effectively in both kinds of languages. After completing this week's quiz, don't forget to watch the Part B Wrap-Up and Part C Preview video.

ML Versus Racket8:53

What is Static Checking?10:00

Soundness and Completeness9:46

Weak Typing9:39

Static Versus Dynamic Typing, Part One9:41

Static Versus Dynamic Typing, Part Two13:47

Optional: eval and quote7:58

教学方

Dan Grossman
Professor

脚本

[MUSIC]

Let's now discuss what static checking is as part of a programming language.

We absolutely need to do this before we discuss the advantages and

disadvantages of having static checking.

After all, nothing is more frustrating than arguing about whether

something is good without understanding what that something actually is.

So I will define static checking as anything that is done to reject some set

of programs even though they successfully parse but before you start running.

So we have the parsing, it's done.

We have the abstract syntax and

our language says, even though it parse, this program is rejected for some reason.

That rejecting process is the static checking.

And which programs are rejected and which ones are allowed to run is absolutely

part of the programming languages definition.

It's in essential part of the definition so

that people know what the legal programs are.

Now you could do static checking in addition to a programming language

definition.

You could have some tools on the side, that also detect bugs and

warn you about them.

And that's a wonderful thing to do that's become very popular, and

I'm very much in favor of it.

But here,

let's focus on static checking as part of a programming language definition.

Now, probably the most common way to have static checking as part of

your language definition is via a type system.

And for type systems,

I want to distinguish in this segment the approach they take from their purpose.

So the approach most types systems take is every variable gets a type.

We use that to type check each expression.

Maybe functions have a type signature that we're interested in and so on.

And that's all fine, and then some programs type check and some don't.

But what is the purpose of this?

We should be very clear about what a particular type of system

is trying to prevent.

For example, maybe it's trying to prevent you from passing a string

to an arithmetic operation like division.

That is one thing that a type system prevents.

It also prevents violating the abstraction of a module like an ML's module system.

It prevents having to do runtime checks like the number question mark

primitive in racket.

It prevents using undefined variables and so forth, okay?

So a dynamically typed language is just a language that doesn't do this sort of

static checking.

Now it's not an absolute line, racket actually checks a couple things.

When you click the run button,

it turns out you're not allowed to have an undefined variable.

But there are very, very few things that it checks statically, and

so we tend to still call it a dynamically typed language.

So to understand this idea of the purpose of a typed system,

let's look at ML a bit more specifically.

Here, I have a long list of things that MLs type checker

has the purpose of preventing.

We know that if an ML program runs,

it will never have any of the following errors.

It will never have a primitive operation used on a value of the wrong type.

For example, you'll never have e1 applied to e2 and

have e1 not evaluate to some closure.

You'll never have an if then else expression where the expression between if

and then doesn't evaluate to a Boole and so on.

You'll never have a variable used that's not defined in the environment when

the interpreter looks it up in the environment, it always finds it.

You'll never have a pattern match with a redundant pattern and so on and so forth.

And a lot of these are standard to type systems, but

they really are part of each programming languages definition.

And different languages can use their type system to prevent different things.

Something prevented by one type system might not be prevented by another, and

that's okay.

It is also the case that no type system prevents everything.

So here are a number of errors,

a number of bugs that MLs type system does not prevent.

It does not prevent calling the head function with the empty list.

It does not prevent array bouncers.

We never say arrays in ML, but it has them.

It makes sure that the subscripting into the arrays always done with an int.

But it does not make sure that that int is small enough

to referred to an element that is actually in the array.

And MLs type system does not prevent division by zero and so forth.

There's a bunch of errors like that, that you can imagine a type system preventing.

But most type systems in today's languages do not.

Now in general, even behind those sort of things,

you never can really expect the type system to find all of your bugs.

Because it doesn't know what your program is trying to do.

Unless a static checker is given a full specification of exactly how your program

is supposed to behave on all inputs.

It cannot possibly read your mind about what the program is supposed to do.

So if you have a perfectly good if then else expression except the then branch and

the else branch backwards.

You put wrong one in the wrong place,

how is the type checker to know that you aren't supposed to do that?

Similarly, if you have two functions of type int arrow int f and g, and

you call one when you meant to call the other one.

Again that's just not the sort of things that a type system is ever

designed to prevent.

So type systems and static checkers are pretty much not substitutes for

the sort of testing and dynamic evaluation of programs that we come to expect.

And unless you had full specification of exactly what you're program is

supposed to do.

So I'm really emphasizing a particular view of type systems here which

is technically accurate and an important perspective on it.

Which is that the purpose of a type system is to prevent certain behaviors

from happening at run time.

And that's a separate issue from how the type checker is defined in terms of

expressions.

So having types and how it's implemented in terms of some recursive procedure that

runs over your program, does type and prints and all the rest of it.

So language design includes two issues.

First, what are you checking, what is the purpose of your type system?

And then second, how are you going to enforce these things?

How are you going to make sure that you never pass a string to the plus operator?

And the hard part of designing type systems

is to make sure that they achieved their purpose.

That while being useful and flexible, and the sort of language people want to use

that the how you do it, correctly accomplishes the what?

What we'll study in the next is the next segment is the exact definition of

correctness and how to think about that.

But before we move on, I like to point out this idea of you can have static checking,

or you cannot have static checking is not the only choice, all right?

But there 's really continuum of options here.

But fundamentally, catching a bug early such as giving a type error before

you've ever run the coding question is always an inherent tension.

Well maybe I shouldn't call it a bug because it's never going to matter.

Programmers don't need to know that,

there's some reason that bug isn't going to occur and so on.

And so static checking, a type system like you're used to and dynamic checking,

when you hit that bad operation at run time are only two points on a continuum.

So to emphasize this, let me pick a strange example, just so

it's not something you're used to.

Suppose we wanted to prevent,

the bad things we're trying to prevent is division by zero.

So you would never have a program get to a point where I try to take 3 and

divide it by 0.

Let me give a range of ways you might prevent this.

The extreme static end would be even before the normal compiled time,

like we've been talking about.

What do we do is every time you try to even type a little bit of your program.

Before it shows those characters on the screen, is would run some analysis to

make sure that the program is currently construed to never divide by zero.

You see how that catches the bug even earlier than we are used to.

We're used to where you type the program and then you chose the compiler and

it give you an error message.

There are also things that are before runtime, but

less eager than we are used to in our type systems.

Like maybe it allows each individual file to type check.

But then it waits and right before you go to run the program,

you have a particular main with a particular set of arguments maybe even.

Then it does some checking and says, you know I think you might divide by zero, so

I'm not going to let the program run.

That would be more eager than the run time we're used to which is sort of how rapid

would do this.

If it would do / space 3 space 0 in parenthesis you would get some sort

of error.

And it seems like, you would think, that's as dynamic as you can go.

You can't go past the division by 0.

We learned in school that you're not allowed to divide by 0.

It's an illegal operation.

And yet we could do lower than that.

We could just somehow, return some answer that indicates we divided by 0.

Return that to callers and have them deal with it.

And that might sound strange, but it turns out it's exactly how floating point

numbers work in pretty much every programming language.

Because the people who do scientific computation

decided that dividing by 0.0 was actually a useful thing to do.

Because if you return infinity then callers might not need it.

It might be that this computation in the case where the denominator is 0.0,

will end up getting cancelled out somewhere else.

Or you'll take some conditional that causes you not to end up using this

variable.

And so it turns out programming images typically do this.

And they could do the same thing with integer 0, if they wanted to.

Because this issue of eagerness, when do you detect bugs and how do you turn

them into errors, is a language design choice and you have a full continuum.

It just so

happens that based on our experience in designing languages over the years.

The compile time and

run time are the two most common points on that continuum to indicate an error.

探索我们的目录

免费加入并获得个性化推荐、更新和优惠。

Coursera 致力于普及全世界最好的教育，它与全球一流大学和机构合作提供在线课程。

© 2019 Coursera Inc. 保留所有权利。

通过 App Store 下载

通过 Google Play 获取

Coursera
关于
管理团队
工作机会
目录
证书
MasterTrack™ 证书
学位
企业版
政府版

社区
Learners
Partners
Developers
Beta Testers
Translators

连接
博客
Facebook
领英
Twitter
Instagram
YouTube
技术博客

更多
条款
隐私
帮助
内容访问
媒体
联系我们
目录
附属公司