ML Type Inference

Loading...

From the course by University of Washington

Programming Languages, Part A

798 оценки

University of Washington

Programming Languages, Part A

798 оценки

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.

From the lesson

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

Meet the Instructors

Dan Grossman
Professor
Computer Science & Engineering

[MUSIC] So, let's now begin studying how ML does type inference, how it figures

out the types for all our bindings. And the way we're going to do this in the

next few segments is via examples. So, given the general algorithm

implementing this and actually showing how it does everything in the whole ML

language, it's a slightly more advanced topic.

It would just take more time in the class than I wish to spend on it especially if

you start supporting things like functions defined in other functions.

But I think these series of examples which we will do manually will be enough

for you to do type inference in your head,

to look at a piece of ML code and in most cases, be able to figure out that type or

understand what the ML type checker is telling you and at least appreciate that

there is complete step-by-step procedure that a computer could implement, that

infers types for code in ML. So, here are the key steps we're going to

see for every example we do. This is how Ml type infrence works.

First, it determines types of bindings in order. So, unless you have mutual

recursion, in which case, it needs to look at all of the things that call each

other at the same time as we'll see in a later segment,

you look at the first binding and further type for it, then the next binding and

further type for that, and so on. And this is why you have to put helper

functions before the functions that use them. Otherwise, you just get a type

error because things simple aren't in the environment yet.

That's the semantics of ML. But we do use those earlier bindings.

We already know their types before we move on the the next one,

and we can use that. Then for each binding,

say, a val binding, or file, fun binding, we have to figure out the type of that

binding. What we do is we analyze the definition

for all necessary facts. These are essentially things that are

going to constrain the type in some way. So, for example, if you see the

expression x > or = 0 inside a function that takes a parameter x,

then x must have type int. We simply look at the, function body in

order to figure out the type of the function overall.

We gather all these facts, we figure out what those constraints imply and

sometimes, they imply things that can't possibly all be true.

That's exactly when you get a type error. If we try to have in our function body x

> or = 0, and x concatenated with the string high, then x has to be an int and

a string, and that's impossible and so you get an error message.

Now, after we've figured out everything the constraints imply and it's, if it's

not a contradiction, so the function or variable will type-check.

Sometimes, we still have too few constraints.

Things that can still be anything, it doesn't matter what type they have.

And that's exactly when we get to infer a polymorphic function, something with a a'

or a b' in it. For example, if you have some function

argument that the function body never uses, then it can clearly be anything, it

doesn't have to be the same as any other type and we can introduce a fresh type

variable for that argument. And then, there is this last step, which

is we have to enforce the value restriction and we're going to ignore

that until one segment later in the section that's focused just on the value

restriction. Alright.

So, here's an example. In future segments, we're going to do our

examples much more step-by-step very much like the actual algorithm does it.

But do get a sense of how these constraints work, let's just keep it

high-level and do this like more how humans would do it.

So, we have two bindings, which we're going to do in order.

First, val x = 42. That's easy.

You see 42, it has type int so x must have type int.

Now, we have this function f, so we know it's going to have some function type.

We have to figure out the types of the arguments and the return type.

So, we just look at the function body. We see if y, then something,

well, y must have type bool. We see z + x, z must have type int,

because x is an int and the only thing you can add to an int is an int.

So great, y is a bool, z is an int. There's a bunch of other things we have

to check. We have to check that this x really does

have an appropriate argument for plus, it does.

We have to check that this 0 has the same type as the type of the expression in the

then branch, it does. So, we're checking all this as

we're doing inference and now, we're basically done.

The entire body here can have type int, so the return type of f will be int. And

then, we notice that w over here never got constrained.

w can be anything. There are no facts that constrain, well,

it has to be in any way, so we know that f must return an int, and we know it must

take a bool, an int, and anything you want.

So, as that sort of last step, we turn that anything you want into a type

variable and we give f this type, bool * int * alpha arrow int.

And if we go over here and try it out, we'll see that that's exactly what the

type checker says as well, okay? So, one more point I want to make,

which is that a central feature of ML type inference is that it does generate

these polymorphic expressions things with type variables whenever it can.

This is great for code reuse and for understanding functions.

It actually tells us in that example that you know, you're never using the argument

w which is why I was able to give it this more general type.

But I want to emphasize because it is often confused, that type inference and

polymorphism with type variables are entirely different concepts, you could

have a language that has type inference and doesn't have type variable.

It would make it harder to infer a type for that previous example but they really

are separate concepts. And conversely, you can have languages with type

variables that do not have type inference, that require programmers to

write down all the types. And Java, in most situations, is a pretty good example

of that. If you want a polymorphic function in

Java, you still have to write down all the types of all the arguments of the

method that happens to be polymorphic.

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

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

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

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

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

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