Hi everyone. This lecture is the last lecture about type inference. Today we are going to implement type-checking of the language TIFAE using unification. You may want to read Chapter 24 type inference in the textbook. This is the language TIFAE that we defined for time being friends with that question mark, right? Now that we learned how to unify two types and how to implement that in Scala in the previous lecture. Now, it's time for implementing a type system, the type checker for TIFAE using unification. When we have a number, it's known T, it doesn't need any call of reunification. Too simple, right? When we have two sub-expressions, E1 plus E2. Now, how do we typeCheck this expression? Previously, we said this one should be the same with this one and those helper functions. Now, we're going to just call unify. Unify these two types because they should be the same. Otherwise, throw an error there. Unify the type of the first sub-expression, e_1 should have typeNumT. Unify the type of the first sub-expression with NumT. Similarly, the type of the second self-expression need to, should have typeNumT. Unify the type of the second sub-expression with NumT. Then if everything is good, there is no error. Then return NumT because that's going to be the type of the addition expression. Simple. It does not really reduce the number of lines of code, but it's declarative. It's very close to this red type system rule. How about Identifier and function expression is just like that because again, there's no call for type check for identifier, but for function, oh, we check the body. Another other thing, because we added usually define types remember, that's why we now have this validated check for this parameter valid type. You may say that weighed in this language called TIFAE, we do not have user-defined types. We do not even need to check the type. Yeah, but in your exam or later in some advanced programming languages, it's safe to check the waveform the type, because it's highly likely that there's a user-defined types. But it is correct that in this particular language, we do not need this affiliate to check. Because we have this type checking of a body expression, we check the type of the body expression, but here we do not have this unify call. Now this is the previous implementation of typeChecking function call. What did we do? We check the type of the first sub-expression f e_1 and get the type, check the second sub-expression e_2, and get the type and do the pyramid tune. It not really declarative. It's not really closely capture that red typing rule. But if we use unify, it's like this. Very simple. Remember, when we first discuss type inference, what did we say when we have function call or sign type variable as a return type, this is what we're doing here. When we have a function call f and a, we make a question mark, or we make a type variable for Results type, which is VarT None. Because it's so simple to call just unify on ArrowType and the type of the function part, meaning that the first topics pressures type F, Tau_1 and Tau 2 should be unified more weight on arrow type of the argument expressions type, and result type. Note that, we can get the type of f. We can get the type of a. Here is a placeholder with VarT None. When we call this unify function, why unifying two types? This result t, this VarT None, we will get some information about the return type and we are going to return it. Isn't a cool? Let me repeat this one more time. When we have a function called e_1 and e_2. Because it's a function call e_1's type should be on a row time. E_2 type should be the type of the parameter type, then the type of the function call is going to be the return type. This is what the red typing rule says. In the previous implementation, we checked the type of the first sub-expression e_1, checked the type of the second sub-expression e_2 and did some pattern matching. It's detailed, but maybe too much. It's not declarative but imperative. The red typing rule is not imperative, it's declarative, meaning that the typing rule says what instead of how. The implementation in the previous version, it was describing how in detail, even though it is not necessary. This aversion is simple because it captures what the rules says closely and saying that, you know what, unify these two types because they need to be the same. What are they? The type of e_1 and the type of argument expression e_2 type and the return type. What's the return type? I don't have it. Make it some type variable and they need to be the same, then why unifying that? We're going to say parameter type should be the same, return type should be the same and the result is going to get the information about the return type of the function part. That's why when we return resT as the result of this case, we're going to get the return type. If it's not clear, we write down concrete example and follow this implementation by yourself. How about if it's your expression? Yeah. Again, so simple. If a zero meaning that you want the value should have some number. We say that e_1 type should be NumT, and e_2 and e_3 type could be anything but they should be the same. That's all. What we say here is that, check the type of the first sub-expression and that should be unified double with NumT. Get the type of the second sub-expression, which should be unifiable with the type of the third sub-expression. If all three things succeeded without any error, then the type of this expression is going to be the type of the second word, the third, which are the same type. Then recursive definition and expression. Remember, here we are defining this recursive function and this expression may use their function. What did we say? Because Tau_1 and Tau_2 are written by programmers, we checked there were from this, we checked their validity, and what? then we make the type of this recursive function, which is going to be parameter type to return type. It's an arrow type from parameter type to return type. Let's call that ft. When we type check the function body, we need to use this extended typing environment. On top of the given environment, we need to add the functions type, and the parameters type to type check the body. Important thing is that the type of this function body should be unifiable with this return type. Then the type of this whole expression is the type of this expression e. So far so good. By using this unified function, we can simplify implementing the type check function by using this declarative style, which is close to the mathematical style used in the typing rule. Time for quiz. Consider the following code. This time type checking of the function call. Where is the question mark? Here it is. When we type check this function call expression, what is going to be the result t in the beginning. Which of the following is correct for this question mark? What do you think? That should be type variable with no information 49, and while doing this unification, we're going to get the information here and then return that information as the result of this type check function call. Thank you.