In this segment we're going to work through a couple examples completely to show type inference. Before we get to the examples, let's make sure we remember the key steps here, right? 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 Emacs buffer, and here's our first example. It's a fairly silly code that just takes in a pair of ints and adds them with absolute value and what not. Of course, type inference doesn't really reason about what the code does, it just collects facts for type checking. So it sees 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 one 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 to 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. And 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, and t3 and t4. So the first thing we see from the pattern match is that T1 has to be T3 star T4. There's no other way for this pattern where we match X against Y comma 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, and so we already know that abs has type int arorw int, and 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.. All right, and that's everything we get from this construct here. Fortunately, getting 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 the equal int. Ha! This is because we added z to an int, okay? So given those three constraints, T1, our argument type to our function is int star int, and we've already inferred the argument type. Now, in terms of the result type, we have that abs of y plus 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 the function, so T2 has to 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 result. 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. Okay? 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 xs' 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 some list, and the first thing has to be an element of the list. So that have to be related like this, and in fact T1, because we are pattern matching against x's, 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, okay? So now we can look at this first branch here, and we can say, oh, in fact, since zero has type int, and that has to be the type of the case expression, and the case expression is the function body, we can know already that the return type has to be int, because zero might be returned. Okay, 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. Okay, so we see that just from here, I'm ignoring here by the way the 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, we just have to deal with the 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'' is a T3 list, so this has to be an int list. And 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 the facts we needed. And it turns out that just from T1 equaling T3 list and T3 equaling int, we know T3 equals int list. And from that and T2 equals int, we know that F has typed int list arrow int, just like we need and just like we want sum to have. So that's our second example. Now what I'm going to do is break this example, so that nothing I did 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 check. 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. 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 that argument type. x and xs' still have to have the form T3 and T3 list for some type T3, because they are part of a list pattern, okay. We still have that T1 has to equal T3 list, and that's because of xs being pattern matched against x colon colon xs'. We still have the T2 as equal int, because of the zero here that's returning it. We still have to have the T3 as 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 this sum of X. So we know from T1 equals T3 list, and T3 equals int, that T1 has to equal int list. All right? 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 is no way to set up additional constraints if that's going to work out. So, I'm going to expect an error message from the type checker, something along the lines of I think x has type int and I think some needs an int list. Now, that's how we did type inference here, and that's the sort of error message 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 the sort of contradiction. The sort of thing where it says int has to the 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 complains about case objects 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 int, honestly, I'm not really sure. I can try to fix that by putting in type annotations or what not, 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, was 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's 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. Okay, 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.