[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 will 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 are the result can still be any type. And we'll use that information to then figure out a polymorphic type where some of the arguments or 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. 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 an int list like we saw in the previous segment. This is just computing the length of a list. But we sort of know what the answer is 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 alpha last arrow int. So we start, as we always do, by saying that length better have type T1 arrow 2. Because it's a function. And its argument better have the argument type. everything continues as we did in the previous segment. We noticed that since, we're pattern matching with x, and xs prime. there's going to have to be some type T3, such that x is type T3. And xs prime as type T3 list, just from that pattern since we have matching against xs, that means the T1, the type of xs has the equal T3 list we know from trying to return zeros of possible result of our function that T2 has the equal int. And let us see that's about it. 1 has type int, so we can have that be an argumentive plus, length is our recursive call, so we better call it with a T1. While xs has T3 list then 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 arrow 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 [LAUGH] used any of the elements, the contents of them here. We could have written an underscore there. Instead if 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 quote a. Arrow int, and that is the type we would give. We would say for all types quote a, or alpha, we can take in a list of quote a's and return an ent. And that's how you type check the length function. The quote 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. its a less interesting function in terms of actually wanting to use it for something. But it's this function f, that takes in 3 arguments, x, y, z, and either returns xyz, or yxz. 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 takes a T1 * T3 -> T4. I could write out more steps and say well it takes one argument and then that argument's 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 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 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 to equal both of those things. So, there's, 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. because I know t1 equals t2, and I want to write down the type for F that incorporates all the restraints I have. Arrow not t4 but what t4 has to equal after all my concerns. 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 infer anything in particular. Between, for T1 or T3 and T1 and T3 do not have to be the same type. So at this point we replace these 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 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 kind of polymorphic type we've seen before, now we just know to infer it and how type inference works for this sort of thing. Okay. So that's our second example, we saw 2 type variables here. Let's do a final example that's actually going to have 3 and is actually 1 of our favorite functions. So here is function composition. We've written this before, it takes in 2 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 argument so let's call that T1 * T2 -> T3 where f has type T1 and G has type T2. Alright 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 the equal depth, 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 x it's going to have to be a function so g is typed 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 kind of function and it's going to have to equal a function that's the return type of G as it's argument so T6 and then some T7 say for what it returns for some T7. Okay, so we 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 a body of 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 all 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. T2 was this 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 > T T5. That's actually a good type for compose. Take in something. g takes in a T4 and returns a T6. f takes a T6, returns a T5. So the whole thing takes in T4. And returns a t5. But we always replace these capital t's consistently, with type variables when 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 we see is T6 so we'll use a for that. Well second thing we see is T5 so we'll use b for that. Third thing we see is T4 so we'll use c for that and now when we 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 paranthesis over here on the right, this is exactly what the repal 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 return to function from c' to b.' So the process was exactly the same as for the other examples. Gather all you facts, constrain everything as much as you can and then replace any unconstrained types consistantly with type variables and that is our examples of type inference.