Hi everyone. Today we are going to learn parametric polymorphism. You may want to read Chapter 22: Parameter Polymorphism in the textbook. Let's see some concrete examples of using parametric polymorphism so to motivate you to learn about the parametric polymorphism. Let's see, what type is inferred for the question mark in the following expression? F is an identity function, so what's the type of this function parameter? Look at the second line. Now we use the function f with the argument number 10 then you know what that question mark should be. That should be our number 10 because the function f takes a number. How about this example? The function is just the same, but the argument is different. Previously, it was the number 10 and now it's a function expression which is the identity function again with the parameter's type number, so what's the type of the function f say in our argument expression? That's an arrow type from num to num. What's the type of the parameter x of f? That's what I just said, num arrow num. So far so good. How about this example? The function f remains the same, but this time we are using f in two places with two arguments of different types. Depending on that dot dot dot if that's a zero, we're going to call f with 10. If that's not zero, then we're going to call f with the identity function with the parameter type number. Then what's going to be the type of the question mark? Is it the number type or numeral num type? We cannot give it a type. No single Tau works for both number and numeral number, but this function does not throw any error at run type if that dot dot dot is some expression of type num. We do like to accept these examples when the question mark could have multiple types, number for f 10 and numeral num for the second call of the function f in this example. How can you do that? That's the topic for today's lecture. Polymorphism. Morphism, meaning some shape. Monomorphism meaning there's only one shape, polymorphism meaning there are multiple shapes. When they say polymorphism in this context, a type could be multiple types of position where a type up here may have multiple different types. We'd like a way to write a type that the color chooses. The function f again takes some parameter x and returns that as it is, but we'd like to represent that the type of the parameter x is what? There could be multiple types and we represent that using this type parameter Alpha. Now function f takes two things; type parameter and parameter. Type parameter Alpha and parameter x, and x's type is going to be that type parameter. What's the type of that type parameter? The function caller can choose it. Let's see this example. When we have this facility type polymorphism s, we can say that hey f you first get actual type and then some value of the type then the body is that. When we call f we need to give it a type of the parameter and pass the value of that type, then this is going to be what? Some expression of type numeral num. The argument part of this again function call this time with f whose Alpha is going to be this type num, then give it an argument expression of type num. This is how we can use function f with two different types. Isn't it cool? Wow, something cool is happening, so this f is polymorphic. F can take argument of different types, that's polymorphic. That big Lambda; this is big Lambda, the Lambda form parameterizes over a type. The small Lambda that form parameterizes over a value. The big Lambda form parameterizes over a type. Meaning that this small Lambda with parameter x takes a value and pick Lambda when type parameter Alpha takes a type. X's place was what? This identity function or number 10 and this Alpha's position was numeral num or num. We use this square bracket notation to represent type argument. Wow many things are happening.Yes so this is a Polymorphic Type. What is the type of this expression now? That function f which it takes a type parameter Alpha and the usual value parameter x whose type is that Alpha and the body expression is x. Then it's going to be an arrow type from the parameter type Alpha to the return type Alpha. It should be something like Alpha arrow Alpha but when we want to call this function it needs a specific type to be called. So far so good? How about this? Function parameter value parameters is still x and the body is still x but now we are expecting two type parameters even though we do not use Beta. It should be something like what? Alpha arrow Alpha but this time it expects two type arguments. We are going to introduce a new type called for all Alpha.Tau this is the notation for this expression. When we have this Lambda Alpha we say that for all Alpha. Alpha arrow Alpha. In this example we have two type parameters, it's going to be for all Alpha. for all Beta. Alpha arrow Alpha. Good then this is the only language with parametric polymorphism. Let's call this Language TpolyFAE, FAE with parametric polymorphism. As usual those red things are new constructs. Two new language constructs for expression e and two new types. To introduce polymorphic types and use polymorphic types. Let's look at this. As we saw before when we introduce a type parameter, we're going to use this big Lambda. This is small Lambda to introduce an identifier as a function parameter. This big Lambda introduces this type parameter Alpha. This is the introduction of a type parameter, this is the use of type parameter. When we have an expression, when it expects a type argument we provide the hype using this square bracket, use of parametric polymorphism. In type now that we can introduce type parameter, we need to be able to write that down and the type of this is going to be worth one more time for all Alpha.Tau of this expression. This is our language for this lecture. So far so good? Yes, very good. Then how do we type check that? It's not that difficult we already discussed how to type-check that using concrete examples so far. One more time there are two language constructs introduced, two types introduced. When we have new expressions we have a typing rule for under type environment Gamma that expression has this type. When you have a new type we say under type environment Gamma, this type is well formed. This and that are different kinds. These two rows are for expressions, these two rows are for types. Are you with me? Yeah, then how do we type check this type parameter Introduction under this given type environment Gamma. Because we are introducing a new type parameter that Alpha should not appear in the domain of the given type environment Gamma. This should be new, that should be fresh. New this is what we mean by that. Then we're going to type check this expression e under this extended type environment. On top of the Gamma we add this type parameter Alpha because we can use Alpha in this e and If the type of e is Tau, the type of this expression is going to be for all Alpha. Tau. So far so good? Yeah, then how can we use the time? We can use the Tau by this expression using this square bracket and Tau 0. How can you type-check this expression? Under this given type environment Gamma, how do we type-check this expression? First, we need to check the validity of this type, Tau 0, and then type-check this expression E under this given type environment Gamma. Because we are giving this type argument, you may be able to guess that the type of E should expect type parameter. Then they are going to be matched. It's going to be for Alpha that Tau 1, meaning that this Tau 1 may use Alpha in there and that Alpha should be Tau 0. That's what we mean by this type application. Then what's going to be the Tau of this expression? Yeah, it's going to be Tau 1, but where Alpha is replaced by Tau 0, just like function call. The type parameter is replaced by type argument in this type Tau. This is how we write that. In this type Tau, if Alpha appears, we replace that with Tau 0. This is how we type-check this type of application expression. How about from this? Type Alpha is formed under the given type environment Gamma if Alpha is defined in the type environment Gamma by what? By this. How do we take away from this? For further Tau under the given type environment Gamma? If we extend the given environment Gamma with Alpha and check the validity of Tau, then this is going to be reformed. Are you with me? If not, please read the textbook. Now that we learned typing rules for these new language constructs is time to use them. Can you type check this expression? This expression uses those new language features in this TpolyFAE language. What is this language? Do you see that? Yeah, it's a simple function, co-expression. Function part, and argument part. A dysfunction part is type application expression with some expression with type argument and this expression is again type parameter introduction with type parameter and another expression so you can type check this expression in this way. Are you with me? Can you do that like this? So this is your homework. I strongly recommend you to type check this expression by yourself. Just put those four typing rules for the new language constructs with new types. On the left and right down on a white paper, saying that under these empty given environment what the type of this expression I'd like to know and you write down this type derivation by yourself. I will just show you some hints then you can finish that. As I said before, because this is a function call expression, we can split that E1 and E2, type check E1, and type-check E2, which is a number. You know how to do. What is this E1 type application expression which is new? Do you remember the typing rule of this type of application expression? We check the validity of the given type argument and then type-check this expression. How do we type-check this expression? This is type parameter introduction expression. Then what did they do? Because we are introducing this new type parameter that should not appear in the given type environment and then we need to type check this expression under this extended type environment and going on so do it by yourself. Then you are going to learn a lot by doing that by yourself. Here's quiz. Consider the following rule. This is the typing rule for type application. Because we gave the type argument Tau 0, we need to check the validity of Tau 0. Because this Tau application, you should expect some type parameter so is type is for Alpha the Tau 1. Then, what's the type of this expression? That is the question. What do you think? Do you know the answer? Just like function call, this type of application also replaces the type parameter Alpha with the type argument Tau 0 in the type Tau 1. Thank you.
