[MUSIC] In this segment, we'll continue with our type inference examples. But the examples here are all going to produce functions with polymorphic types. So the key ideas, we'll start the same, we're still going to collect all the facts we need for type-checking. We're still going to use these facts, to constrain the type of the function. The only difference is, we'll end up with so few constraints, that some of the arguments of our result can still be any type. And we'll use that information to then figure out a polymorphic type. Where some of the arguments and results might need to be the same type as some others, or not. And then we'll have inferred polymorphic functions. So even though this is conceptually perhaps more difficult, it's actually easier ,because we have fewer constraints to deal with, all right. So let's just go over here, and let's start with an example that's a lot like the sum of the elements in the int list that we saw in the previous segment. This is just computing the length of a list, but we sort of know what the answer's going to be. We know that length on a list can work for any type of list, so we'll be building up to showing a list -> int. So we start, as we always do, by saying that length better have T1 -> T2, because it's a function, and its argument better have the argument type. Everything continues as we did in the previous segment. We notice that since we're pattern-matching with x, and xs'. There's going to have to be some type T3 such that x has type T3, and xs' is type T3 list, just from that pattern. Since we are pattern-matching against xs, that means that T1, the type of xs, has to equal T3 list. We know from trying to return 0 as a possible result of our function, that T2 has to equal int. And let's see, that's about it. 1 is type int, so we can have that be an argument to plus. length is our recursive call, so we better call it with a T1. While xs' has type T3 list, and we already know that T1 = T3 list. So we have no more constraints, everything type-checks with what I've already written down. Therefore, putting all those constraints together, I end up with T3 list -> int, and there's nothing more to say. There's no constraint on what T3, the type of the list elements of xs, need to be. After all, we never used any of the elements. The contents of them, here, we could have written a underscore there, instead of x. So when we have a type like this, and it cannot be further constrained? What we do is we take all these T's that are in there, there's one in this case, and we replace them consistently with type variables. So in this example, we take that T3, we replace it with the first letter of the alphabet, 'a, -> int, and that is the type we would give. We would say for all types 'a, or alpha, we can take in a list of 'a's and return an int. And that's how you type-check the length function. The 'a simply falls out, from having no reason to prefer any particular type for the list elements, okay? So now, let's do a more sophisticated example. It's a less interesting function, in terms of actually wanting to use it for something. But it's this function, f, that takes in three arguments, x, y, and z, and either returns (x, y, z) or (y, x, z). Now you can look at this function and say, well, if true, it's always going to return this one. But the type-checker follows the type-checking rules. And the type-checking rules for a conditional is, that we don't know which branch might be returned. So, let's just go through this and pretend we're the computer, doing type inference. So, f, I'm going to go ahead and say it takes a T1 * T2 * T3 -> T4. I could write out more steps, and say well, it takes one argument, and then that one argument is a pattern. But if you just look at this, it's going to have to take in some triple and return some fourth type, T4. And certainly, x1 has type T1, y has type T2, and z has type T3, okay? So at this point, we don't need to type check this is true, that is type bool, just like if/then/else needs. And we just noticed that we're either going to return this, or we're going to return this. So T4 either has to have type T1 * T2 * T3, or T4 has to have T2 * T1 * T3. And in fact, those both have to be true, because the type-checker doesn’t know which of these might happen. So the result type has to be the type has to be the type of (x, y, z) and the type of (y, x, z), so both these constraints have to be true. And the only way those can both be true is if T1 = T2, right? There's no other way for T4 for to equal both of those things. So that's enough, then we'll have the same thing in both cases. So if we put it all together, the type of f is T1 * T1 * T3, aecause I know T1 equals T2. And I want to write down the type for f, that incorporates all the constraints I have. -> not T4, but what T4 has to equal after all my constraints, so T1 * T1 * T3. And what this type says, is that x and y have to have the same type, z can have a possibly different type. So there are no other constraints, there's no reason to prefer anything in particular for T1 and T3, and T1 and T3 do not have to be the same type. So at this point, we replace these capital T's with 'a and 'b, consistently. So we can pick any letters of the alphabet, but every T1 has to be 'a, and every single T3 has to be 'b. And so we end up with this type, which is actually correct. You can call this with any types of arguments you want, but x and y have to have the same type. z can have the same type, or it can have a different type. It's exactly the sort of polymorphic type we've seen before, now we just know how to infer it, and how type inference works for this sort of thing. Okay, so that's our second example, we saw two typed variables here. Let's do a final example that's actually going to have three, and is actually one of our favorite functions. So here is function composition. We've written this before, is takes in two function arguments, f, g, and returns a function that takes in an x and returns f (g x). And type inference will work for this just fine. compose takes a pair for its arguments, so let's call that T1 * T2 -> T3, where f has type T1, and g has type T2. All right, now we just need to look at this function body, and see that it is a anonymous function. So we have this argument x, and it's going to have to take in some T4. And the body, being a function, has type T4 -> T5. The body of compose here has to be some function, and that has to equal the return type of compose. So let's say that T3 has to equal that, okay, for some T4 and T5. So from g being passed x, which has type T4, we actually know that T2, which is g, g has to be a function. If you're going to write g space x, it's going to have to be a function, so g has type T2. T2 is going to have to equal T4 -> T6 for some T6. T4 is the type of x, okay. So now, from f being passed the result of g, T1, the type of f, is also going to have to equal some function. And it's going to have to equal a function that's the return type of g, as its argument, so T6. And then some T7, say, for what it returns, for some T7. Okay, we've looked at everything. But now we have to say, from f being the body of the anonymous function. Remember, our anonymous function was this T4 -> T5. From a call to f being the body that function, we know that T7, the return type of f, has to be equal to T5, the return type of that anonymous function. Because we call f, and then that's our result, okay. So now we can just put it out together, so put it all together. We end up with the T1, the type of f, has to be T6 -> T5, because we just decided T7 = T5. We had T2 = T4 -> T6, that was the type of g. And T3, which is our result for compose, well, that's T4 -> T5, okay? And if we actually put this all together, just for T1 * T2 -> T3 here. What we end up with is (T6 ->T5) * (T4 ->T6) -> (T4->T5). And that’s actually a good type for compose. Take in something, g takes a T4, returns a T6, f takes a T6, returns a T5, so the whole thing takes in a T4 and returns a T5. But we always replace these capital T's consistently with type variables shen we're all done, there are no additional constraints here. So let's just use a, we'll just go left to right. So the first thing that we see is T6, so we'll use a for that. The second thing that we see is T5, so we'll use b for that. The third thing that we see is T4, so we'll use c for that. And now when see another T6, we have to use a again. And when we see another T4, we have to use c again. And when we see a T5, we have to use b again. And except for these unnecessary parentheses over here on the right, this is exactly what the repl will print out, as the type for compose. It's something that takes in a function from 'a to 'b, and a function from 'c to 'a, and returns a function from 'c to 'b. So the process was exactly the same as for the other examples. Gather all your facts, constrain everything as much as you can. And then replace any unconstrained types consistently with type variables. And that is our examples of type inference.