[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.