Hi everyone today, we're going to learn a new language called T R F A E. Can you guess what it is? Of course it's with F. A. And types and what is it for our our for Rikers shin, you may want to read chapter 20 of the textbook typing recursive functions. So there are ego languages and lazy languages. Right. Do you remember that? So in lazy languages it may not be the common to have real word lazy languages. Have you ever used any lazy language? Yeah, there is Haskell. I think that's the only real word lazy program language. And there are some lace other lazy languages and but there are no lazy languages that permit mutation. There are no lazy languages without type system. Why not? Why? What do you think in a lace language function courts are not necessarily value weighted in the order where they appear in the code. In eager languages. It's really easy to see which code is going to be evaluated when because it's in order in the text. However, for functions that perform side effects, it matters in which order they are executed. So in ego languages it's relatively easy for us to understand what effects are going to happen in which order because it's eager. But in lazy languages it's not like that. So lazy languages usually emulate those side effects in special types that ensure that they are executed in the right order. That's usually called Monette. If you are interested in that topic, I recommend you to study Haskell. That's going to be fun. We are discussing types. Right? Yeah. And there are two kinds of types. Static types and dynamic types. Actually, dynamic types are not really types because we do not check or guarantee anything with their dynamic types. There are values at runtime and there's techs are just dynamic types. Some languages have static types. Other languages have dynamic types and what are their pros and cons. Right. Yeah. So static typing, it means that we check languages, we check programs before actually running the code. That's what we mean by stating before run time at compile time. That means that's what we mean by static static typing. Can detect errors early only meaning before evaluating the code and by having static checking static typing, we can get some information about the program. So we can optimize this could before running, which leads to efficient execution. And because types describe the properties of programs, it actually provides documentation, it's actually better documentation of code than comment. How about dynamic typing? Dynamic typing, meaning that we do not check, were, you know, guarantee anything before actually running the code. We only get some checking at run time. What is it good for dynamic typing because we do not get any checking at compile time. It's really fast in production of coding, meaning that it allows rapid development and easier to adapt to changing requirements. If there are some added demands from clients, then we can change that really easily compared to static typing, which requires checking of the new demands in these days because you know, we like to have both benefits from static typing and dynamic typing. There are languages with benefits from both words like typed, record, meaning. Record as a dynamically typed language with some static checking typescript and flow meaning javascript with some type checking diamond bag stage and others. So that's a new trend. And I think typescript and flow and other variants are much better than javascript. Okay, that's why we call type check before inter inter meaning actually running the code. So we do not want to run bad code. So before calling the inter function, we call the type check function to prune out bad programs if possible. So we already saw this analogy at run time. Under a given environment sigma. We evaluate an expression E getting a value V at compile time as an analogy to the environment sigma. We have the type environment gamma Under gamma the type environment. We check the type of an expression E and get its type tao the tao should be the type of the value V. That's what we have been doing. Then Finally, the concept for today. Record version actually, you know, record version. We learned the record version in the first part of discourse programming languages and if you remember there was a helper function to make some function recursive called MK rec. I'm not going to go into the details of this function if you are not sure about this function. Go check the previous video. All I'd like to say is that it is not possible to tie check the previous expression in T F a or even in t p f a with pairs. Why not? I will ask you to try to find some type for dot dot dot because nothing works in place of dot dot dot. Remember in the previous lecture when we discussed pairs, when we try to simulate pairs in D f a t f a, we couldn't do that. We could simulate pairs of two numbers were pairs of two billions Were two pairs of two values with the same time. Yeah, it was okay to simulate that using T f a e, even though the code was ugly and long. But if we want to simulate a pair of two values of different types, it was not possible. So what did we do that? We extended the language to have pairs as language constructs. Same here. We do like to simulate record version in T F a but it is not possible because of the limitation of its simple type system then what can we do? Yeah, we need to extend the language and the type system. When the type system rejects your code, which does not throw any error at run time, it may be time to extend your language and the type system in this case we are going to add a recursive function definition with the cured D E F. Do you remember that? We wanted to add a conditional expression When we introduce a recursive function. Why do you remember that? Yeah, if there's a record version we need a branch. When some condition holds. We like to call the function recursive, li when the condition does not hold, it does not matter Which one holds or who Does not. In one way we need to be able to call the function recursive lee in the other way we need to stop. Otherwise it's going to be an infinite loop and the program does not stop does not terminate. It does not produce any result. So we need a branch to stop record version and produced a result. So when we introduced this D E F recursive function definition, we are going to add a conditional expression if 01 more time. Remember it's not if but if zero meaning that the condition part is going to be a number and when the numbers value is zero because it's zero. If the viability of any zero, we are going to evaluate the second sub expression. Otherwise we're going to evaluate the third self expression. That's our language. This is our language. TFAE with F zero and recursive function definition. Now we are going to call this language T R F A Are you ready? Okay, this is our you know A S T for T R F A. Nothing surprising. Right? If zero expression has a conditional expression part. Troop branch false branch. Recursive function has a function? Name, parameter name, party expression and an expression that may use this recursive function here are two new bits parameter type and return type. Okay, are you with me then, interpretation is just as usual. Right? It's not that difficult as you can see if zero we interpret the first sub expression. If the value of it is known with zero, interpret the true branch. Otherwise interpret the false branch for recursive function definition. We ignore the parameter type and return type ignore with this underscore because it's interrupt at runtime at runtime. We do not care about types because these parameter types and return types are going to be checked at compile time by the type check function before calling this inter function. If there was an error or problem with these two types, we are not going to call this function the inter Right, okay. Then interpretation is going to be the same as before then. How are we going to type check this new expressions if zero, as I said before. If zero has three sub expressions you on E 2 80 three everyone's value should be a number. So we say that the ones type is going to be numb. It is values type I don't care about all I care is that it is type and if this type should be the same which is the type of this zero expression, that's what this red influence rule says. Let's implement that. Yeah, The first of expression If zero or C. That type should be number and what do we need to do next? We need to check the types of the second and the third of expression TNF we're going to check their types and all we need to say is that they should be the same. They must be the same. Then we are done. Do you remember those hyper functions most same, Same and no tie. Right. We already saw that in the previous lecture. If you're not sure, please stop here and try to understand them and then move on to check type checking recursive function. Again, we'd like to know it's typing rule. Don't panic. It's not that difficult. Let me try to help you with this rule under a given type. Environment gamma. We have this recursive function definition and it's used. We are defining a recursive function named X. F. Which has only one parameter and its body and we may use that recursive function in this expression E and yeah, this function body is going to be E. F. And function has again one single parameter. X whose type is Taiwan. And the functions body E F. Type is tau two meaning that this X. F. Type is an aero type because it's a recursive function right, aero type from what parameter type Taiwan to return. Type tao too. So first a good if you understand this then, you know everything When we have the gene expression. We first need to check whether the function bodies type is actually what we expected. We wanted to be what this return type type two. Under which environment on top of the given type. Environment gamma. We'd like to add two pieces of information. The recursive function name X. F. And the parameter X. Y. Because in the function body we may recursive call the function and we may use the parameter and we already know the prime. The functions type is Taiwan to tell two and parameters type is Taiwan with that information. With all this information we are going to type check this function body that should be told to. Okay then when we have a good looking function definition, we may use it. So in this expression E we'd like to check what the type of E E is. When we take type check this E we may use the recursive function. So on top of the given type environment gamma we add the information about this recursive functions, time and type check it. The type of that expression is going to be the type of this whole expression. Note that we didn't add exit the primaries type in here. Why not? Because in this expression parameter is not available unlike the recursive function body. Okay so first a good let's implement that first as I just wrote before, we first make an arrow type from parameter type to return type. That's going to be the type of this recursive function named F. So we we extend this given type environment with this recursive functions type. Then what's next? Then we'd like to check it's the return type R. T. With what? With what? With the type of the function body with the type of the function body. How do we check the type of the function body? We can check the type of the function body under this type environment on top of the given time. Environment with the type of the function and what the piece of information? The type of the parameter. So we need to extend that to this one more time. We're going to tape check the function body on top of the given type environment, the type of the reclusive function and the type of the parameter. So for a second finally we are going to type check this expression on the rich type environment. This which is not the same with the previous one. So what is it going to be on top of the given type environment? We only add the type of the recursive function which is anti E M. V. So yeah. Now you know what's going to happen next. That's it. This is how we are going to type check the expression. So first a good Yes, that's it. This is how we can define a language for T. F. A A with Rikers. Rikers asian and how we interpret that? T. R. F. A. Language and type checking here's chris consider the following code the codes that we just saw. Type checking a recursive function definition and its use. So we already saw this code and are following rules for type checking the recursive function. How did we do that remember? Yeah. Under this given type environment we type checked this recursive function definition and use of it. Right. The question is when we type check this function body, what's going to be the environment? That's the question. Do you know the answer? What is it? Yes. On top of the Given type environment, gamma. We need two pieces of information. The type of the recursive function and the type of the parameter. Thank you.
