1 00:00:06,100 --> 00:00:09,350 Here's a question for you. How many natural numbers are there? 2 00:00:10,510 --> 00:00:13,002 Put it this way. If I'm using a natural number to 3 00:00:13,002 --> 00:00:17,498 represent your position in line, how big could that be? 4 00:00:17,498 --> 00:00:18,762 One? Ten? 5 00:00:18,762 --> 00:00:22,706 1000. That's a pretty long lineup, but it could 6 00:00:22,706 --> 00:00:25,995 be. The answer is that there's an arbitrary 7 00:00:25,995 --> 00:00:30,610 number of natural numbers. We just don't know how big it could be. 8 00:00:32,170 --> 00:00:35,592 And what that tells us is that we ought to be able to design a well-formed 9 00:00:35,592 --> 00:00:39,610 self-referential data definition for natural numbers. 10 00:00:40,690 --> 00:00:43,923 And what that tells us, is we ought to be able to design a lot of functions on 11 00:00:43,923 --> 00:00:48,564 natural numbers really easily. That's what we're going to do in this 12 00:00:48,564 --> 00:00:50,925 video. First I need to tell you about a 13 00:00:50,925 --> 00:00:53,890 primitive function where I kid you not, you might not have seen yet. 14 00:00:53,890 --> 00:00:58,784 I'll add one. And lets see 0 is 0. 15 00:00:58,784 --> 00:01:10,150 Add one of 0 is 1. And add 1 of add 1 of 0 is 2, and so on. 16 00:01:10,150 --> 00:01:14,940 So, add 1 takes a natural number and adds 1 to it. 17 00:01:14,940 --> 00:01:17,980 And there's another function. Sub 1. 18 00:01:17,980 --> 00:01:25,247 If I take sub 1 of 2, I get 1. And when I take sub 1 of sub 1 of 2, I 19 00:01:25,247 --> 00:01:31,360 get 0. In a funny kind of way, add1 is a little 20 00:01:31,360 --> 00:01:34,735 bit like cons. Cons takes a short list and gives you a 21 00:01:34,735 --> 00:01:40,590 list one longer. And sub1 is a little bit like rest. 22 00:01:40,590 --> 00:01:44,430 Rest takes a list that's at least one long, and gives you a list that's one 23 00:01:44,430 --> 00:01:48,688 shorter. So, think of add1 as building a natural 24 00:01:48,688 --> 00:01:53,812 number up to the next biggest natural number, and think of sub 1 as taking a 25 00:01:53,812 --> 00:02:00,554 natural number down to the next smallest natural number. 26 00:02:00,554 --> 00:02:06,122 I mean naturals starter dot racket, and what I have here is a self referential 27 00:02:06,122 --> 00:02:11,853 data definition for natural. Previously we took the type natural to be 28 00:02:11,853 --> 00:02:16,187 primitive. Now, we're giving a definition for that 29 00:02:16,187 --> 00:02:20,410 type. And it says look, a natural is 1 of 0. 30 00:02:20,410 --> 00:02:23,870 That's the base case for natural, right? That's the smallest natural. 31 00:02:23,870 --> 00:02:30,120 Or it's add 1 of natural. So, if you look at the examples, example 32 00:02:30,120 --> 00:02:37,699 n 0 is 0. And natural 1 is add 1 of n0, that's 1. 33 00:02:37,699 --> 00:02:40,834 And add 1 of n1 is 2, and I think you could clearly see here, I can get a 34 00:02:40,834 --> 00:02:47,340 natural number as big as I want this way. This well-formed self-referential data 35 00:02:47,340 --> 00:02:54,580 definition will let me build up to as big a natural number as I want. 36 00:02:54,580 --> 00:02:58,090 But I also have to be able to take a natural number back apart. 37 00:02:59,230 --> 00:03:00,800 And I already told you how that's going to work. 38 00:03:00,800 --> 00:03:04,805 Add 1 makes it bigger, sub 1 is going to make it smaller. 39 00:03:04,805 --> 00:03:09,760 So, now let's look at the template. Template rules used. 40 00:03:09,760 --> 00:03:14,579 It starts with a one of in two cases. So, that got me the con. 41 00:03:15,660 --> 00:03:20,438 The first case is atomic distinct zero. There is a predicate zero question mark 42 00:03:20,438 --> 00:03:25,074 in DSL that tests whether a number is zero, so that got me the zero question 43 00:03:25,074 --> 00:03:32,804 mark and the dot dot dot. And then, as I said, there's kind of this 44 00:03:32,804 --> 00:03:37,340 funny compound, this funny cons-like thing, add1, that takes a natural and 45 00:03:37,340 --> 00:03:42,966 makes the next biggest natural. So, I'm treating this as a compound. 46 00:03:42,966 --> 00:03:46,248 But it's a funny compound, because there isn't first and last. 47 00:03:46,248 --> 00:03:51,820 There's just, there's just rest. There's just sub1. 48 00:03:51,820 --> 00:03:57,232 So, there's the self-reference because once I strip the add1 off with sub1, I'm 49 00:03:57,232 --> 00:04:01,520 left with a natural. So, that's the self-reference in this 50 00:04:01,520 --> 00:04:04,290 type comment. That's the self reference rule. 51 00:04:04,290 --> 00:04:09,372 And the presence of that self reference is why there's a natural recursion here 52 00:04:09,372 --> 00:04:13,462 in the template function. Now, I've got a little bit of the 53 00:04:13,462 --> 00:04:16,950 template commented out here. Just ignore that for now. 54 00:04:16,950 --> 00:04:19,745 What the part that's not coming out is what the template rules are telling us to 55 00:04:19,745 --> 00:04:23,922 produce. So, now we've got the type comment, the 56 00:04:23,922 --> 00:04:27,335 well form self referential type comment and we've got a template. 57 00:04:27,335 --> 00:04:32,810 Let's design some functions that operate on naturals. 58 00:04:32,810 --> 00:04:39,210 Let's see, the first one is a function that consumes natural, and it produces 59 00:04:39,210 --> 00:04:45,240 the sum of the naturals up to and including n. 60 00:04:45,240 --> 00:04:48,580 Let's see. That's going to be a natural because if 61 00:04:48,580 --> 00:04:55,714 you add up any number of naturals you get a natural. 62 00:04:55,714 --> 00:05:07,493 Reduce some of natural 0 n inclusive. Define, we'll call it sum n and the stub 63 00:05:07,493 --> 00:05:11,550 is 0. Let's see check expect. 64 00:05:11,550 --> 00:05:15,420 This is a self referential data definition. 65 00:05:15,420 --> 00:05:19,790 So, our first check-expect should be for the base case which is 0. 66 00:05:19,790 --> 00:05:29,364 The sum of 0 to 0 is 0. We need one that's at least two long, in 67 00:05:29,364 --> 00:05:34,640 this case two long means at least two in size but lets just do sum of one for now. 68 00:05:35,690 --> 00:05:40,775 Well, lets see if I add up 0 and 1, that's 1. 69 00:05:40,775 --> 00:05:54,230 Lets do three now. So, let's see, if I add 0, 1, 2 and 3. 70 00:05:54,230 --> 00:06:00,350 That's that, which is 6. There's some good check expects. 71 00:06:00,350 --> 00:06:06,380 They fail, but they're well formed. Let's get this template. 72 00:06:06,380 --> 00:06:14,186 Copy it down, and I'll take this part that isn't supposed to be there out. 73 00:06:14,186 --> 00:06:21,620 We'll rename the template, rename the natural recursion. 74 00:06:21,620 --> 00:06:24,160 And let's see, what am I supposed to do here? 75 00:06:25,600 --> 00:06:32,710 The base case result is 0 and what does sum do? 76 00:06:34,700 --> 00:06:37,070 Well, these I actually kind of put in the wrong order, didn't I? 77 00:06:38,620 --> 00:06:42,520 This really happens in the other order, because we start with the big end and we 78 00:06:42,520 --> 00:06:47,211 go down. So, this is really 3, 2, 1, 0. 79 00:06:47,211 --> 00:06:53,911 The natural recursion, in this particular case, the natural recursion is going to 80 00:06:53,911 --> 00:06:59,420 be, this is going to be the sum of plus 2 1 0. 81 00:06:59,420 --> 00:07:04,688 That's going to be the natural recursion. So, what do I have to do with the natural 82 00:07:04,688 --> 00:07:07,609 recursion in order to get the result I want? 83 00:07:10,810 --> 00:07:13,722 Oh, I see. I have to add, and then there's something 84 00:07:13,722 --> 00:07:17,000 missing from the template, which is actually n. 85 00:07:17,000 --> 00:07:20,568 I need n. I'm allowed to add it to the template. 86 00:07:20,568 --> 00:07:26,990 Remember, a template is a skeleton of what you have available. 87 00:07:26,990 --> 00:07:31,742 In this case, the template didn't show us that we had the entire n available, but 88 00:07:31,742 --> 00:07:35,500 we do have it available. Let's try it. 89 00:07:36,940 --> 00:07:40,070 All three tests passed. Okay. 90 00:07:40,070 --> 00:07:43,054 Let's do the other one. What we need to do is design a function 91 00:07:43,054 --> 00:07:47,494 that consumes natural number n and produces a list of all the naturals of 92 00:07:47,494 --> 00:07:52,230 the formed cons and cons n minus 1 all the way down to empty but doesn't include 93 00:07:52,230 --> 00:07:56,161 0. Okay. 94 00:07:56,161 --> 00:08:04,130 Let's do that. Consume natural, produce ListOfNatural. 95 00:08:04,130 --> 00:08:07,770 I'm not going to do a data definition for list of natural because we're producing 96 00:08:07,770 --> 00:08:12,450 it, not consuming it, so I don't need the template for it. 97 00:08:12,450 --> 00:08:15,150 I think you could produce the data definition for a list of natural if you 98 00:08:15,150 --> 00:08:17,985 wanted to do it right now, it's not necessarily needed for a simple list type 99 00:08:17,985 --> 00:08:25,443 that we're going to produce. So, produce cons and cons n minus 1 all 100 00:08:25,443 --> 00:08:32,324 the way down to empty. Not including 0. 101 00:08:32,324 --> 00:08:42,980 Define we'll call it to-list. And it'll produce empty as its stub. 102 00:08:42,980 --> 00:08:46,374 Let's do some examples. Well, again, we'll start with the base 103 00:08:46,374 --> 00:08:52,387 case. Oops, not to-list of empty, it consumes 104 00:08:52,387 --> 00:08:56,630 natural. Produce is empty. 105 00:08:56,630 --> 00:09:00,345 So, let's see. To-list of 0, it's not supposed to 106 00:09:00,345 --> 00:09:05,007 include 0, the base case, so 0 is the base case, but we don't include it, we'll 107 00:09:05,007 --> 00:09:09,192 produce empty. See that's kind of funny what's going on 108 00:09:09,192 --> 00:09:11,221 there. Let's do the next one, just to be sure we 109 00:09:11,221 --> 00:09:14,488 have it clear in our mind. To-list of 1. 110 00:09:14,488 --> 00:09:18,960 Well, lets see, we're never suppose to include 0 in the result. 111 00:09:18,960 --> 00:09:23,120 But there's nothing that says we're not suppose to include 1 in the result. 112 00:09:23,120 --> 00:09:27,090 So, this looks to me like it should be cons 1 and empty. 113 00:09:27,090 --> 00:09:32,430 And that makes sense because the next number after 1 will be 0. 114 00:09:32,430 --> 00:09:36,830 That's going to produce empty. So, it's cons 1 onto the result of the 115 00:09:36,830 --> 00:09:41,370 natural recursion, empty, that looks pretty good. 116 00:09:41,370 --> 00:09:45,302 The rule is we have to do one that is at least 2 lon, though, so let's do that. 117 00:09:45,302 --> 00:09:54,280 2 list of 2 is cons 2 cons 1 empty. That looks pretty good. 118 00:09:54,280 --> 00:09:58,130 Let's run 'em to be sure they're well-formed. 119 00:09:58,130 --> 00:10:03,150 They fail, so they're well-formed. We'll go up here and get the template 120 00:10:03,150 --> 00:10:07,970 again. Cmd+E lets me see more space. 121 00:10:11,410 --> 00:10:13,830 I'll take out this part that the template's not supposed to have in it. 122 00:10:13,830 --> 00:10:21,734 I rename the template and the natural recursion. 123 00:10:23,310 --> 00:10:27,431 Let's see. The base case result is empty. 124 00:10:27,431 --> 00:10:32,640 And what's the result in the case of recursion? 125 00:10:32,640 --> 00:10:37,884 Well, I'm so used to cons. This is always, that's the natural 126 00:10:37,884 --> 00:10:44,525 recursion in the case of 1. That's the result of the natural 127 00:10:44,525 --> 00:10:48,230 recursion in the case of 2, so I'm supposed to cons the current number 128 00:10:48,230 --> 00:10:56,350 itself onto the natural recursion. Run that and it works. 129 00:10:56,350 --> 00:11:00,240 Whoops, I forgot to comment out the stub. Op. 130 00:11:00,240 --> 00:11:07,600 All six tests pass. Now, at this point, having done two of 131 00:11:07,600 --> 00:11:11,200 these, or maybe after I wait 'til I've done ten of them, but if you do ten of 132 00:11:11,200 --> 00:11:17,250 them, you'll see that it's always nice to have the actual natural number. 133 00:11:18,680 --> 00:11:26,808 So, even though the template rules themselves didn't put it in the template, 134 00:11:26,808 --> 00:11:34,301 what I'm going to do now is go back to the template and put it in, along with a 135 00:11:34,301 --> 00:11:48,564 note that says; template rules don't put this in, but it seems to be used a lot. 136 00:11:48,564 --> 00:11:53,260 So, we added it. The key thing that happened in this video 137 00:11:53,260 --> 00:11:59,739 is we had this insight that is an arbitrary number of natural numbers. 138 00:11:59,739 --> 00:12:04,741 So, that means a well-formed, self-referential data definition should 139 00:12:04,741 --> 00:12:11,235 describe the natural numbers. So, that produced a template with a 140 00:12:11,235 --> 00:12:17,330 natural recursion in it. And once we had that template for the 141 00:12:17,330 --> 00:12:23,840 natural recursion, these functions actually were super-easy to write. 142 00:12:23,840 --> 00:12:26,375 So, have some fun writing some more of these functions that operate on natural 143 00:12:26,375 --> 00:12:28,680 numbers. I think you'll find that they go pretty 144 00:12:28,680 --> 00:12:32,270 quickly, because the template really gets you almost all the way there. 145 00:12:33,470 --> 00:12:36,968 Once you've practiced those, then go back to some of the harder stuff we did this 146 00:12:36,968 --> 00:12:40,720 week, especially having to do with the reference rule. 147 00:12:40,720 --> 00:12:44,490 The reference rule is the place so far where working systematically helps you 148 00:12:44,490 --> 00:12:48,376 the most, because it really helps you break what would otherwise be complicated 149 00:12:48,376 --> 00:12:53,041 functions into two parts. So, be sure you follow that reference 150 00:12:53,041 --> 00:12:53,690 rule.