Here's a question for you. How many natural numbers are there?
Put it this way. If I'm using a natural number to
represent your position in line, how big could that be?
One? Ten?
1000. That's a pretty long lineup, but it could
be. The answer is that there's an arbitrary
number of natural numbers. We just don't know how big it could be.
And what that tells us is that we ought to be able to design a well-formed
self-referential data definition for natural numbers.
And what that tells us, is we ought to be able to design a lot of functions on
natural numbers really easily. That's what we're going to do in this
video. First I need to tell you about a
primitive function where I kid you not, you might not have seen yet.
I'll add one. And lets see 0 is 0.
Add one of 0 is 1. And add 1 of add 1 of 0 is 2, and so on.
So, add 1 takes a natural number and adds 1 to it.
And there's another function. Sub 1.
If I take sub 1 of 2, I get 1. And when I take sub 1 of sub 1 of 2, I
get 0. In a funny kind of way, add1 is a little
bit like cons. Cons takes a short list and gives you a
list one longer. And sub1 is a little bit like rest.
Rest takes a list that's at least one long, and gives you a list that's one
shorter. So, think of add1 as building a natural
number up to the next biggest natural number, and think of sub 1 as taking a
natural number down to the next smallest natural number.
I mean naturals starter dot racket, and what I have here is a self referential
data definition for natural. Previously we took the type natural to be
primitive. Now, we're giving a definition for that
type. And it says look, a natural is 1 of 0.
That's the base case for natural, right? That's the smallest natural.
Or it's add 1 of natural. So, if you look at the examples, example
n 0 is 0. And natural 1 is add 1 of n0, that's 1.
And add 1 of n1 is 2, and I think you could clearly see here, I can get a
natural number as big as I want this way. This well-formed self-referential data
definition will let me build up to as big a natural number as I want.
But I also have to be able to take a natural number back apart.
And I already told you how that's going to work.
Add 1 makes it bigger, sub 1 is going to make it smaller.
So, now let's look at the template. Template rules used.
It starts with a one of in two cases. So, that got me the con.
The first case is atomic distinct zero. There is a predicate zero question mark
in DSL that tests whether a number is zero, so that got me the zero question
mark and the dot dot dot. And then, as I said, there's kind of this
funny compound, this funny cons-like thing, add1, that takes a natural and
makes the next biggest natural. So, I'm treating this as a compound.
But it's a funny compound, because there isn't first and last.
There's just, there's just rest. There's just sub1.
So, there's the self-reference because once I strip the add1 off with sub1, I'm
left with a natural. So, that's the self-reference in this
type comment. That's the self reference rule.
And the presence of that self reference is why there's a natural recursion here
in the template function. Now, I've got a little bit of the
template commented out here. Just ignore that for now.
What the part that's not coming out is what the template rules are telling us to
produce. So, now we've got the type comment, the
well form self referential type comment and we've got a template.
Let's design some functions that operate on naturals.
Let's see, the first one is a function that consumes natural, and it produces
the sum of the naturals up to and including n.
Let's see. That's going to be a natural because if
you add up any number of naturals you get a natural.
Reduce some of natural 0 n inclusive. Define, we'll call it sum n and the stub
is 0. Let's see check expect.
This is a self referential data definition.
So, our first check-expect should be for the base case which is 0.
The sum of 0 to 0 is 0. We need one that's at least two long, in
this case two long means at least two in size but lets just do sum of one for now.
Well, lets see if I add up 0 and 1, that's 1.
Lets do three now. So, let's see, if I add 0, 1, 2 and 3.
That's that, which is 6. There's some good check expects.
They fail, but they're well formed. Let's get this template.
Copy it down, and I'll take this part that isn't supposed to be there out.
We'll rename the template, rename the natural recursion.
And let's see, what am I supposed to do here?
The base case result is 0 and what does sum do?
Well, these I actually kind of put in the wrong order, didn't I?
This really happens in the other order, because we start with the big end and we
go down. So, this is really 3, 2, 1, 0.
The natural recursion, in this particular case, the natural recursion is going to
be, this is going to be the sum of plus 2 1 0.
That's going to be the natural recursion. So, what do I have to do with the natural
recursion in order to get the result I want?
Oh, I see. I have to add, and then there's something
missing from the template, which is actually n.
I need n. I'm allowed to add it to the template.
Remember, a template is a skeleton of what you have available.
In this case, the template didn't show us that we had the entire n available, but
we do have it available. Let's try it.
All three tests passed. Okay.
Let's do the other one. What we need to do is design a function
that consumes natural number n and produces a list of all the naturals of
the formed cons and cons n minus 1 all the way down to empty but doesn't include
0. Okay.
Let's do that. Consume natural, produce ListOfNatural.
I'm not going to do a data definition for list of natural because we're producing
it, not consuming it, so I don't need the template for it.
I think you could produce the data definition for a list of natural if you
wanted to do it right now, it's not necessarily needed for a simple list type
that we're going to produce. So, produce cons and cons n minus 1 all
the way down to empty. Not including 0.
Define we'll call it to-list. And it'll produce empty as its stub.
Let's do some examples. Well, again, we'll start with the base
case. Oops, not to-list of empty, it consumes
natural. Produce is empty.
So, let's see. To-list of 0, it's not supposed to
include 0, the base case, so 0 is the base case, but we don't include it, we'll
produce empty. See that's kind of funny what's going on
there. Let's do the next one, just to be sure we
have it clear in our mind. To-list of 1.
Well, lets see, we're never suppose to include 0 in the result.
But there's nothing that says we're not suppose to include 1 in the result.
So, this looks to me like it should be cons 1 and empty.
And that makes sense because the next number after 1 will be 0.
That's going to produce empty. So, it's cons 1 onto the result of the
natural recursion, empty, that looks pretty good.
The rule is we have to do one that is at least 2 lon, though, so let's do that.
2 list of 2 is cons 2 cons 1 empty. That looks pretty good.
Let's run 'em to be sure they're well-formed.
They fail, so they're well-formed. We'll go up here and get the template
again. Cmd+E lets me see more space.
I'll take out this part that the template's not supposed to have in it.
I rename the template and the natural recursion.
Let's see. The base case result is empty.
And what's the result in the case of recursion?
Well, I'm so used to cons. This is always, that's the natural
recursion in the case of 1. That's the result of the natural
recursion in the case of 2, so I'm supposed to cons the current number
itself onto the natural recursion. Run that and it works.
Whoops, I forgot to comment out the stub. Op.
All six tests pass. Now, at this point, having done two of
these, or maybe after I wait 'til I've done ten of them, but if you do ten of
them, you'll see that it's always nice to have the actual natural number.
So, even though the template rules themselves didn't put it in the template,
what I'm going to do now is go back to the template and put it in, along with a
note that says; template rules don't put this in, but it seems to be used a lot.
So, we added it. The key thing that happened in this video
is we had this insight that is an arbitrary number of natural numbers.
So, that means a well-formed, self-referential data definition should
describe the natural numbers. So, that produced a template with a
natural recursion in it. And once we had that template for the
natural recursion, these functions actually were super-easy to write.
So, have some fun writing some more of these functions that operate on natural
numbers. I think you'll find that they go pretty
quickly, because the template really gets you almost all the way there.
Once you've practiced those, then go back to some of the harder stuff we did this
week, especially having to do with the reference rule.
The reference rule is the place so far where working systematically helps you
the most, because it really helps you break what would otherwise be complicated
functions into two parts. So, be sure you follow that reference
rule.