Explore
For Enterprise
Join for Free
Log In

Обзор
Поиск
Для организаций
Войти
Присоединиться бесплатно

ML Type Inference

Loading...

Programming Languages, Part A

Вашингтонский университет

4.9 (оценок: 1,101) | Зарегистрировано учащихся: 67K

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.

Просмотреть программу курса

Получаемые навыки

Recursion, Higher-Order Function, Pattern Matching, Functional Programming

Рецензии

4.9 (оценок: 1,101)

5 stars
1,040 ratings
4 stars
54 ratings
3 stars
1 ratings
2 stars
1 ratings
1 star
5 ratings

AL

Mar 22, 2017

Great course!\n\nI think this course has just the right balance of theoretical background, formal definitions, and actual examples to make "just right".\n\nThanks Dan, and everybody else involved!

SK

Mar 24, 2017

An excellent course! Make sure you really have enough time to take this course. There are a lot of videos, but they worth watching. I'd recommend this course to everyone involved in programming.

Из урока

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

Текст видео

[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., 2019 Все права защищены.

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

Coursera
О проекте
Руководство
Карьера
Каталог
Сертификаты
Сертификаты MasterTrack™
Степени
Для организаций
Для правительственных организаций
Для стационара

Сообщество
Learners
Partners
Developers
Beta Testers
Translators

На связи
Блог
Facebook
LinkedIn
Twitter
Instagram
YouTube
Технический блог

Еще
Условия
Конфиденциальность
Помощь
Доступность
Пресса
Контакты
Справочник
Филиалы