Hi everyone. Today, we are going to learn type inference. Chapter 24 of the textbook is type inference. Let's start with some quiz. What is the type of the following expression? Lambda x.x +1. What do you think? What's the type of this expression? Yeah, yet another three questions. It's not really an expression in our language because parameter doesn't have any type of notation, right? Yeah, but you know, it's time [INAUDIBLE] its type should be, right? Yeah, x we are adding 1 to x, so X's type would better be number. Then x type is number and the body's numbers it's going to be no matter num, we know what it should be. So, that's what type influence does. In our current language, we require programmers to write down types. Most statically typed languages, prefer to have type annotations by programmers because that relieves the job of type checking. But programmers are lazy, I am lazy. We do not want to write down all the types that's not for people, but for computers. So that's what type inference does for us. Type inference is the process of inserting type annotations where the programmer omits them. So as you can guess, it's not always possible. There should be some minimum amount of type and there are some places that people can omit type annotations. Let's see. So we will use explicit question mark in our program to make it clear where types are omitted in reel world programming languages, there's no question mark. It's just lambda x.x + 1. But to make our study clear, to let you know where types are omitted, we're going to use explicit question mark. So this is our language and our type, right. Number, boolean, arrow type and question mark, meaning, hey, here should be some type, give me that type information. So let's start with some examples again, as we saw before. Lambda x.x +1, what's the type of that question mark? The place to their. So let's call it T1. Let's set up some equation, right? It's that's an unknown variable T1, X's type is unknown variable T1. I know the type of 1, which is number. So I know X plus one's type should be number. So, which infers the type of that unavailable T1 which is num. So the type of this function expression is num arrow num. This is how a type influence works. So in general, it creates a new type valuable, unknown valuable for each question mark. And change type comparison to install type equivalences, meaning that we added some unknown valuable here and there, everywhere. So, by using all ready known facts about types, we set up more equations to solve the equations. Are you with me? We are making up set up equations with some unknown valuables, and try to solve those equations to get the types for those question marks. Okay, how about this? So as we saw before, true's type is boolean, 1's type is number and X's type is this unknown valuable T1, right? Let's see. True is boolea, 1 is number, X's type is T1. Then, if true, 1, X should be what? If true, 1, X should be number, because we know that those two branches should have the same type. Meaning T1's type is number. Then we know that this is again, numeral num, easy. How about this? Remember back in high school we learned equations maybe in middle school, depending on your country. And there are cases where equations have, education has only one solution or many solutions or no solution at all. [FOREIGN] We are going to discuss that here. Type inference is solving equations, this time impossible cases. Why? Because look at that, we know that X's type is going to be T1? We know the true branch T1 type is number. So first branch X's type should be number, right? But, at the same time the condition part X should be number, right? Wait, boolean, right? Then X's should be both boolean and number, are you with me? One more time. Here, X's type is T1, then because tree branches number that should be number, but this is not if [INAUDIBLE] but if, that should be boolean. Meaning that this 21 should be both boolean and number. How come? No way. So there's no time. T1 cannot be both boolean and number at the same time. It's impossible. Aha, how about many cases? Here, X's type is T1, X's type is T1. So I know that this function expressions type is T1 arrow T1. But what is it that T1? Yeah, what type would it be? I don't know. It could be numeral nun, boolean bool, Numeral boll, whatever. Any arrow type whose primary type and data type are just the same. So the type checker leaves valuables in the reported type, just like that. It's any type 2 the same type, identity function, right? Okay, then now let's move on to the highlight of our usual cases, function call. Here, function part is just the same expression that we just saw, right? It's going to be T1 arrow T1. We have no other further information. How about the second sub expression, this is a function expression manipulating numbers. So it's time it's going to be num arrow num. Really? That's going to be the argument of the first function expression, whose type is it going to be numeral num. So T1 is going to be, what do you think? Yeah, numeral num, then the first sub expressions type is to numeral num to numeral num. This is numeral num. The whole expression is going to be, what? Yes. Numeral num, not that difficult, right? Okay then, how about this? It's a function expression. Well, I can start right, X's type is going to be T1, that I know. Another thing, I know 7's type is number, what's next? There is not much information, right? There's a function called x and seven. What can you do? Here's another hint, when we have a function call, When we do not have any further information, give it a type valuable T2, then we can move on, right? Why? Because, X's type is T1, and argument's type is number. When you say it's applications type is T2, we knew that X's type is going to be what? An arrow type from number 2, T2. That's our 3. Then, T1's type. This parameters type is norm arrow T2. The party type is what? T2. So the type of this function expression is what? What do you think? Yeah, numeral T2 to T2. What did I do? In general, create a new type valuable for the result of a function call. That's all we did. That's it. Very simple, right? Now, one last tricky question, cyclic equation. What is that? It's a function expression. It takes a parameter X. In the function body, we have a function called function part there's x and argument part there's x. The X's type is T1, X's type is T1. And what's the type of x and x? It's a cyclic equation, right? Can you resolve this equation? I cannot, in our current type language? So X apply to X, no type, because T1 cannot be T1 arrow dot dot dot .They cannot be the same. T1 cannot be number because norm is not an arrow type. T1 cannot be boolean because boolean is not an narrow type. Suppose that T1 is T 2 to T3, T2 must be T1. It's a cyclic, we cannot resolve this problem. We can do this when we have more enriched, advanced type system, but not here. If you want to know more, check for the references. Here, we are going to just say uh-uh, there is a problem. We cannot infer its type. And how do we do that systematically? We are going to discuss that in the next lecture. So here is quiz. Which of the following is the type of lambda x:?.x7? We saw this before, right? What's the type of x T1? What's the type of 7 number? What's the type of X7 T2 dot dot dot. You can do this, right? Yes, then what's the answer? Yeah, the last one. Thank you. [MUSIC]
