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