Tip:
Highlight text to annotate it
X
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 h ere'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 thos e
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 one, 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 gonna evaluate all of the arguments, E1 up
through en. So you're gonna get values. So when we had something over here, like, pow
of two, and 22. plus two. We looked up pow to get a function
binding. Then two is already a value. Then we go ahead and eagerly evaluate 22 plus
two to four So the body, when we call pow, it's only gonna see a four. It's gonna
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 two and four, we end up evaluating this function body in
a dynamic environment where X is bound to two, Y is bound to four, and pow is bound
to the function itself. So as always when we introduce a language construct, no matt
er how simple or how complicated, we can understand it completely with syntax type
checking rules and evaluations rules, and that's functions.