[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.