[SOUND] In our last segment we learned how to define functions like the functions pow and q that you see here that we wrote and we learned how to call functions like you see at the bottom with cube of four and you see in the bodies of q where we called pow and in pow where we called pow. So we got a sense of how to write these things, but I want to take a more formal look, because one of the things I'm trying to teach you is how to give precise understanding to what constructs in a programming language mean. So let's just jump in and look first at that function binding. When you define a function, what's the syntax, what are the type checking rules, and what are the evaluation rules? Okay, so the syntax in general, is the keyword fun, F U N. Then a variable, which will be the name of the function. Then, the list of arguments, which for now we'll have the variable name, colon, type, separated by commas, inside parentheses, then the equal character, and then an expression, any expression you want, as deeply nested as you want, with all sorts of sub expressions, and that E is what we call the function body. Let me do evaluation rules next, because this is so simple. it may seem strange. A function is already a value. When we have a function binding, we add X zero to our dynamic environment, so that later expressions can call that function, and that's all we do. We don't evaluate that function body until we call the function, and that's a different language construct. we'll do next. So, take away message, a function is already a value. Alright. Type checking is not as simple, so let's think about how this works. Alright? The end result of type checking a function body, so we're going to take that function name, called X0 here on the slide, and we're going to add it to the static environment, with the type, takes arguments T1, T2, T3 up to Tn, and returns a T. When you see the function syntax here with T1 star, separated arguments by star, and then an arrow for the T. If the function binding type checks appropriately. And here's how we type check that function body. Basically, we type check E, using everything that was already in the static environment, because E can use any earlier bindings, and it gets to use the argument, so it knows x1 has type t1, x2 has type t2 and so on. And, since we allow functions to be recursive, x0 can be used be in E. It is in the static environment and it has the type of the function overall. Okay? That last one might seem a little bit magical, since the type checker has to figure out the type of x zero. but we'll learn later in the course that it's not so magical. It's one of the neat things that ml can do for us. Alright, so let's go into a little bit more detail on the type checking here so we do have this new kind of type, t1 star for all the arguments, then the arrow and the t. So that's the result type of the function over on the right. The overall type checking result is to give x0 this type, and those arguments, X1 and X2, those variable names. Those are not added to the static environment for after this binding. They're only in the static environment for the body of the function. That's probably not too surprising. That's how methods work in Java or functions or methods in Python or anything else. Those arguments are only in scope or only in the static environment for E, not for the code after this function definition. Okay? Next, because the evaluation of a call to x zero is going to return the result of e, that type that is the return type for the function, t, is the type that e has. So, what the type checker does is it type checks e, it gets some type, and then that's the return type for x zero. And as I already man-, mentioned, this is a little bit magical, since we never wrote down t. the type checker is just able to figure it out, and we'll have to discuss later in the course, how it is able to figure it out. Okay, so those are function bindings, how we define functions. It turns out we added another construct to our language, and that's calling a function, using it. And those, so those function calls also have a syntax, type checking, and evaluation rules. So let's go through those. When we had a function call, let me show you here in the code. So something like pow X Y minus 1, or here's another function call, or here's one, or here's one, there's a couple more, alright? The way we always wrote those is with one expression which is what function we want to call, and then some other expressions in parentheses and separated by commas, and those are the arguments we're calling the function with. So when we had something like pow of two and two plus two. The first expression, pow, we'll look that up in the dynamic environment to get a function, and then these other arguments we'll evaluate and those will be the arguments of the function. But that's getting ahead to evaluation rules. Syntactically, it's just expression and then more expressions in parenthesis separated by commas. You don't need the parenthesis if there's exactly one argument, but if there's a zero or two or three or four, then you do. That's the syntax. Type checking, how do you type check a function call? Well rule number one, E zero better have a function type. It better have a type that has that arrow in the middle, with the arguments on the left, and the result on the right. Assuming it does, then we type check all of the other expressions. E1 up through en. There better be the right number of them for the function that we're calling, and each one better have the right type for the function that we're calling. And if that's all true, then the result of the function call is the result type of e zero. So it would have type t, as indicated here on the slide. So that's why, when we had something like pow of x comma y minus one in that recursive function, it ended up having type int, and let's see why here. Because we have this call here, so we look up pow, and pow itself has type int star int, arrow int. So fortunately, we're calling it with two arguments, and when we type check X, we look it up in the static environment, which here in the function body has type int. Then we have to type check Y minus one, which similarly we have type int, because we can look up Y and then subtraction takes two ints. So the call type checks, and the result of the call, will have type int, because that is indeed the result type of the function we're calling. Okay, so that's type checking. Evaluation rules are also interesting for a function call. So here's what we do, there is really three steps to evaluating a function call. First, evaluate E0 to figure out what function you're going to call. So if you're going to call pow, you're going to look up pow in the dynamic environment, and you're going to find the right function binding. Second, you're going to evaluate all of the arguments, E1 up through en. So you're going to get values. So when we had something over here, like, pow of two, and 22. plus 2. We looked up pow to get a function binding. Then two is already a value. Then we go ahead and eagerly evaluate 22 plus 2 to 4 So the body, when we call pow, it's only going to see a four. It's going to have no idea how we got that four as the result of an addition. So that's step two. And then step three is to actually evaluate the function body. Now how are we going to evaluate that function body, like the body of pow? We're going to extend the dynamic environment that was there back when we defined the function with extra values for the arguments. So X will be two and Y will be four. In general, are the end arguments to our function X one, X two up through X N end up with the the value, being bound to the values for this call. The first value argument, the second value argument, the third value argument. And lastly, inside that function body, any recursive calls are bound to the function itself. And so that's why when we do something like call pow with 2 and 4, we end up evaluating this function body in a dynamic environment where X is bound to 2, Y is bound to 4, and pow is bound to the function itself. So as always when we introduce a language construct, no matter how simple or how complicated, we can understand it completely with syntax type checking rules and evaluations rules, and that's functions.
