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.