[MUSIC] In this segment, we're going to work through a couple of examples completely to show type inference. Before we get to the examples, let's make sure we remember the key steps here. The idea is to just collect all the facts we need, all the facts that have to be true for something to type check and use those to constrain the type of the function. So we're going to do two examples. Neither of these examples will involve polymorphism. And then, I'll change one of the examples so in fact it doesn't type check at all. And we'll see how type inference can figure that out as well. So, for the rest of the segment, we'll just do this over here in the Emax buffer. And here's our first example, it's a fairly silly code. It just takes in a pair of ints and adds them with absolute value and whatnot. Of course, type inference doesn't really reason about what the code does, it just collects facts for type checking. So it see a function binding F and the first thing it realizes is for some types, T1 and T2, F has to have type T1 arrow T2, why? Well it must be a function. And we know all functions take 1 argument. So that just has to be. And in fact, if we look at the pattern, which is just a variable here for that argument. X has to have type T1. There's no other way this function binding is going to type check. So now we can go on to the function body and start gathering additional constraints. And we first see this binding here. And we say okay, I have two other variables I'm going to have to figure out types for. So y is going to have to have some type T3 and z is going to have to have some type T4. Now we can start looking at all the expressions and patterns in our program to come up with additional constraints among these types T1, T2, T3 and T4. So, the first thing we see from the pattern match, is that T1 has to be T3 * T4. There's no other way for this pattern, where we match x against the pattern (y,z) to type-check. So, [else pattern match does not type-check]. We can write down these reasons as we go just to keep track of what we're doing. Okay. So the next thing we could look at is this function call here. Now remember we've already type checked all earlier bindings including things that are built into the environment. So we already know that abs has type int arrow int. So for abs of y to type check y is going to have to have type int which means T3 has to equal int. T3 being the type of y, T3 equals int. And that's everything we get from this construct here, fortunately you get an int back, because plus will require that. And that means that this expression over here will have to be an int. And since that's z, we know that T4 has to equal int. This is because we added z to an int. So given those three constraints, T1, our argument tied to our function, is int * int. And we've already inferred the argument type. Now in terms of the result type, we have the (abs y) + z has type int. So the let expression has type int. So the body of our function has type int. And we know that T2 has to be the type of the body of function. So T2 has the equal int and once we've constrained T1 and T2, that's the type of f. Which is what we were supposed to be inferring and we have our results. So we just gathered facts and continued to propagate those constraints until we had the type we needed for f. So now let's go on and do a more interesting function a function that's actually useful for something. And that's summing all the elements in a list. So it's going to start the same way sum is a function. So it has to have type T1 arrow T2. The argument has to be that T1. And now we're just going to look at these three lines, which actually have quite a bit of information about what T1 and T2 need to be. So first because we pattern match a T1 we know that these other variables x in that pattern has to have type T3. And x is prime has to have type T3 list. And the reason why, sorry, excuse me, is that if we have this pattern here it can only match lists. We know the second thing has to be sum list and the first thing has to be an element of the list. So they have to be related like this and in fact, T1, because we are pattern matching against Xs, has to equal T3 list. There's no other way for just the patterns, just the things on the left of the arrow to type check. So now we can look at this first branch here and we can say in fact since zero has type int. And that has to be the type of the case expression, the case expression is the function body. We can know already that the return type has to be int because zero might be returned. So we know our result type, now we just have to look at this other branch and figure out what's going on there. So we know that T3 has to equal int, why? Because x has type T3. And we add x to something. So we see that just from here. I'm ignoring here, by the way, that plus works on type real as well. That's an issue I'm going to ignore in this segment, but that's okay. So we have quite a bit here. And we just have to deal with this (sum of xs'). And in fact, everything we already know is enough to type check this. So we know T3 is int. We know xs prime is a T3 list so this has to be a int list. An int list is T3 list which is T1. That is the argument of sums so this recursive call already type checks. This recursive call has to give back a T2. We know T2 is int. And that's good because that's the argument to plus. So it turns out we don't get any new facts here, we already had all of the facts we needed. And it turns out that just from T1 equalling T3 list and T3 equals int, we know T3 equals int list. And from that and T2 equals int, we know that f has type int list arrow int. Just like we need and just like we want some to have. So that's our second example. And now what I'm going to do is break this example. So that nothing I do it here is wrong this is correct. Now let's go and change our code and see what type inference would do in that case. So I'm going to make a mistake here, a mistake that will not type chart. If I make this mistake it will type check, it will just be an infinite loop. I'm more interested in this mistake, where I try to recursively call sum with the head of the list. And this is, in fact, now not going to type check. So let's see why. Everything starts how it did before. Sum still has to be a T1 arrow T2, xs still has to be the argument type. X and x's prime still have to have the form T3 and T3 list for some type T3. Because they are part of a list pattern. We still have the T1 has to equal T3 list and that's because of xs being pattern matched against x colon, colon xs prime. We still have the T2 equals int because of the zero here that we're turning in. We still have to have the T3 is int because we're adding it right here. And now we're in a very interesting situation. So, let me delete this and just focus in on the (sum x). So we know from T1 = T3 list and T3 = int the T1 has the equal int list. We also know that T3 equals int. And that is the type of x. So now I have to try to call something that needs an int list. With something of type int. And that cannot type check. There's no way to set up additional constraints, so that's going to work out. And so I would expect an error message from the type checker. Something along the lines of, I think x has type int, and I think sum needs and int list. Now that's how we did type int here. And that's the sort of error message that we would get if we went in this order. But the type inferencer sometimes has a bit of a mind of its own if you will in the sense that it can gather constraints in any order it likes. That will not affect its final result which is a deep property that's very cool. But it will report an error as soon as it gets to a situation where it reaches this sort of contradiction. The sort of thing where it says, int has to equal int list and I know that's impossible. So, in fact when I try this out I think we'll see a different error message in a different place in the code, and that's okay. I mean, you might not like it, but in some sense there are too many facts here for them all to be true. And the type error message is just going to tell you about one of them. So if it goes in a slightly different order, I think it actually can claim about case object and rules don't agree. It says that the I think what it's saying is that it thought this was going to be a list and something else was an end. Honestly, I'm not really sure. I can try to fix that by putting in type annotations or whatnot. But it's actually complaining up here that it figured out that xs is going to have to have type int because of how we called it down here. But now you're matching it against an int list. So all it really did if I had to guess is it worked on these facts before the pattern matching facts so you got a different error message. But it always detects because this is how type inference works that there is no way for the entire thing to type check. And so it gives you one error message about where it ran out of room to try to figure out a good answer. So that's our examples of working through type inference. We'll see more examples next where we're going to end up with polymorphic types for the results of our function.