Hi, everyone. Today we are going to learn yet another new language called TVFAE. This language is really cool because finally, you can define your own types. Let's see how you can do that. The relevant part in the textbook is Chapter 21, Algebraic Data Types. Let's start with some example. As before, we are going to see some examples that simulate new feature, this time variance. We'd like to see some simple examples that can be simulated by our current language. But the last example is going to be the example that we can assimilate using our current language so that it motivates us to introduce our new language construct. Let's look at this first example. It's an example of moving some petition. It's either left, how many steps, or right, how many steps. Left meaning that it takes a number, and produces a pair. Because it's left, we'd like to make a pair of zero and that amount. Is going to be another pair starting with one and then amount. Left meaning a pair of zero and some number, right meaning a pair of one and some number. When we get some value of a pair, we can check whether it's to left or right by taking the first component of the pair value. So far so good. Then this displacement function takes a pair, it's going to be either left, how many steps, or right how many stems and then returns the amount. It takes a pair, it checks whether the pair's first component is zero or not. If zero checks whether the value of p at one, the first component of the given pair is zero or not. If it's a zero, it's left, so we're going to say that left meaning zero minus how many steps the second component of the pair. Left is going to be minus negative numbers, meaning positive numbers. It's going to just return the value. Then we can make a displacement with this open left to five. It's going to have what? Minus 5. So far so good. Then let's look at another example. This time, we can still have a pair of different pipes. Meaning that let's assume that we'd like to have a function pass hard. Question mark is going to be called pass hard, meaning that when you have some grading or pass-fail, then we are going to be able to tell you whether you passed this course or not. One more time. Pass hard asks whether you can pass this course or not, and there are two criteria; either you're grading or your pass-fail result. With grading, if your grade number is larger, greater than 70, you pass in this example, not in this course. Pass fail, meaning a Boolean value, true or false. If it's true, you pass, otherwise, you fail. Great, meaning that we get some grading number and we're going to make a number and a pair. Why? Because in this pair, the first component again describes whether this pair is representing great or pass-fail. If it represents grading, the pair starts with zero. If this pair represents pass-fail result, it starts with one. The second component is going to be yet another pair. But if it's great, it contains a number. If it's PF, pass-fail, it contains a Boolean value. But because we need to have both of them, there should be some junk value. Meaning that if it's a grade, we have a pair of zero and another pair in this pair. Only this grading number is important, and these Boolean value, it means nothing. Because we do not check the value. In this pf value in this pair, the first component is one, denoting that this is for pf, third grade. The second component is a pair with what? True or false. This is important whether you pass or fail, but the great part is not important because we are not going to use that. We need to make up a value for the other type, which is annoying. Are you with me? We disperse the whole function takes a pair, and check the first component. If it's a zero, it's for grading. Then check whether the grading is greater than 70. Otherwise, it`s for pass-fail, then check whether it's pass or fail. How did we get the value? It's the given pairs, second component, first component. It`s the given pairs second component, second component. We can do this, but it's annoying, it's not pretty, but it's still doable. Here is another example that we cannot simulate this using our current language, which is recursive data types. Not recursive functions, but recursive data types. Do you know what it is? Do you have any concrete example of that? Yeah, list? Our list is either empty or not. Empty list has no elements. Non-empty list has at least one element, and another list. Our list is either empty or not. Non-empty lists consists of at least one element, and another list. This another list, meaning recursive datatype. We are defining our list using another list. That's what we mean by recursive data type. That's the example that we cannot simulate. Let's try to do that. When we have empty, let's make a pair of zero, and something. For a non-empty list, let's make a pair of one, and another. Then what is it going to be this x and y? What's going to be the type of this dot dot dot? Can you have such a type for recursively defined time? Can you tell me a hint? Maybe not, because it's not possible in our language. What can you do? What I like to do is something like this in Scala, and other language, I am going to show you what we want to represent in this Scala version. In Scala, we can define a type trait NumList, list of numbers. It's going to be either of these two cases, either empty or non-empty, with one number element, and another list. Again, we are defining NumList using NumList that`s a recursively defined type. How do we use that? This is a recursive function named len. When we take a parameter of type NumList, then we match this LSD whose type is NumList. Because its type is NumList, we know that it's either the empty or cons. We can pair a match with this argument value. Saying it's going to be either empty or not. Just like that, right? You must be familiar with this example. Then similarly, what we'd like to do is to have our own language to represent the same thing. In our new language, we're going to add two new language constructs for defining types, and using types. We're going to define our own types in this language by using a language construct with the keyword type and write down your type name, which has two variance. Again, a type may have two or more variants, but in this language, we are going to require every type to have only exactly two variants. Why? To simplify your language, and it's going to be the first variant's name empty, second variant's name cons, and they will have only one field or more time to simplify the language. Here we're saying that empty has a number argument, cons, has a pair of argument, cons has a one number and another numlist that recursively define the type. Empty does not need to take any field, but just to simplify the language we'll require that. We can define a type, and we can use that newly defined type by using pattern matching. Just like in the previous example with Scala, we can define a recursive function with this parameter lst, whose type is numlist. We can pattern match its value with empty and cons, this is going to be their fields value. If it's empty, do this, otherwise, do that, and function call. Wow, so in this new language, we can define our own user-defined type and use that just like Scala. Wow, that's a cool language, which is TVFAE, this is going to be our language for FAE with types and variance. The language looks similar to you, it has number-related expressions, function-related-expressions, recursive functions, and now those rare debates, type definition and use, introduction of user-defined types, and user of that. Just like we already saw in the previous example, type is the keyword, after the keyword, we have the type name key. In the previous example, numlist equals, it has two variants, x_1 and x_2. Empty and cons of value of type t is going to be either x_1 something or x_2 something. They should have only one field of tie, Tau 1 and Tau 2 respectively. Using this type, we are going to evaluate e, that's how we introduce type. Pattern matching, we have an expression A whose type should be some type t. If we know the type of e, we know which variants it may have, x_1 or x_2. We know that each variant has exactly one field, so it's going to have their field values. If it matches the first variant, evaluate the second sub expression. If we match the second pattern, then evaluate the third sub-expression. Are you with me? One more time. We are defining a new type name t numlist for example, which has two variants, for example, empty and cons. They should have only exactly one field of type number, for empty or pair of number and numlist for cons, using this information, we evaluate this expression. While evaluating this expression, we may use type t empty cons. In this expression e, we may have this pattern matching, some expression is type maybe numlist, then we know that it's going to be either empty or cons. If it's empty, we know it should have one number, if it's empty, evaluate this. If it's cons, we know it has a pair of number and numlist, then evaluate that. So far so good? Now that we can define a new type name, we are going to introduce a type name t, type ID, type identifier, and a type could be now a number, an arrow type or type name t numlist. Another addition is two values. A value is either num number n, or closure v, or some value of type t. Here, x is going to be constructor, those variants M2 Cons with some value, that's going to be constructor. Then what is this angle bracket x, it's going to be a constructive value is, which expecting an argument value. Let's see what I mean. Here's our language in scholar. It has so many fields, but as the syntax says, type definition has a type name, I will show you. Type definition has the time name numlist. The first variance name, empty. Second variance name, cons. First, variance fields type, num. Second variance field type, a pair of numbers, numlist. Then finally an expression. You can see the correspondence between the concrete syntax and this extraction text, no, you better do that. Metric expression pattern match It has some expression of tie numlist, then the constructor is going to be either empty or cons. If it's empty, its fields value is going to be bound to this name. If it's cons, it's fields value, which is going to be a pair to be bound to here. If this expression is empty, evaluate his expression, otherwise, it evaluate this expression. That's it. One more time you'd better be able to make a correspondence between this concrete syntax, e match blah blah blah with this abstract syntax. You should be able to do this by yourself. Then here's a value. One more time, we added two values, variant and construct. Variant value takes a constructor name in argument value, which makes a variant value of type T. Construct value is the name of the variant and expecting an argument value, so far so good? Then let's interpret those new expressions. Let's interpret that. One more time, in type definition, we have type names and type notations. We may define a new type T we define this new type T has two variants, x1 and x2, and their field types are tau1 and tau2, those types are ignored at runtime. At runtime, we do not care about the new type name, the type of the field of the first variant, the type of the field of the second variant we do not care. All we care is evaluate e. When we evaluating e, we may encounter x1 and x2, so we need the values of them, but we don't care about the types. When we interpret this expression e, we're going to get a value. Then on the rich environment, on top of the given environment Sigma, we add two pieces of information for x1 and x2. What is x1? What is x2? What are their value? X1 value is, yes, constructor. Constructor, with name x1. X2 is value is our constructor with name x2. Using that information, interpret this e, evaluate e, get a value that's going to be the value of the whole expression. Then we can interpret this expression e on the rich environment one more time on top of the given environment on top of the given environment, add two pieces of information. What are they? The value of the first variance name, the value of the second variance name. The first variance name, the second variance name, what are their values? Their constructor v with their names, so far so good? Yeah. We're just making constructors, waiting for argument values. Then we need to make arguments values and construct values meet to make variant values. How do you do that? Now just like continuation call, here, when we have e_1 e_2, this time e_1 could be closure V or constructor V. Remember when we run the continuation, when we have function calls and texts e_1 and e_2, you e_1's value could be either CloV or ContV in this T V FA E, where we have our function calls and texts e_1, e_2, e_1's value could be either CloV or ConstructorV. ConstructorV, then what can we do with it when we have CloV? You know what to do. When we have a ConstructorV, we are going to get the value of the argument expression as usual, and make VariantV. When ConstructorV gets an argument value, we make VariantV. One more time. When our ConstructorV meets an argument value, it creates this VariantV. Then now it's a value. ConstructorV is also a value but waiting for an argument value, but now it does not wait for anything. So far, so good. Then finally, now that we introduced the types, let's use types. Pattern matching. Let's see the semantics. Under a given environment Sigma, when we have this parametric expression, that long, we first interpret the first subexpression e_0. Let's interpret that. What's its value? Its value is going to be what, either empty or cons. If e_0 type is num list, it's going to be either empty or cons. When we defined a new type called flower. There are two kinds of flower like rose or lily. Then when we have a parametric of an expression e_0, whose type is flower that we know that it's either rose or lily naturally, because that's how we defined the type called flower. We know that when we interpret e_0 it's going to be either x_1 or x_2 because these parametric says is x_1 or x_2. Otherwise, that example is going to be rejected at compile time. How? We're going to see that later. Today, we're just interpreting it. If e_0's value is x_1 with some argument, then that argument value of v is going to be bound to this x_3 and interpret e_1. Are you with me? Interpret e_1 on top of the given environment we need to add this information saying the field's value is going to be v, and get the value that's going to be the value. If e_0's value is what? Second variant. Then interpret the second part. We're under this environment. That argument value is now bound to this x_4. Not surprising. How do we implement that? These cases expression has all those components. Interpret the first sub-expression. Then it's going to be a VariantV, otherwise an error. It should be VariantV. It should be either first variant or a second variant, otherwise error. It should be either empty or cons. It should be either rose or lily, not tulip, not sunflower. Then we evaluate the corresponding expression under this extended environment accordingly. I'm pretty sure you can understand this. Otherwise, write down this red rule and blacks color implementation, and try to make the correspondence. If that doesn't help read the textbook. Here's quiz. Consider the following code. This is the function call with variance. This rule says that when we have e_1, e_2, e_1's value is not CloV but ConstructorV. It is very easy. Then what's the value of e_1 e_2? What do you think? Yeah, that should be VariantV. Thank you.
