1
00:00:00,919 --> 00:00:05,180
welcome back an well we're going to do
now

2
00:00:05,180 --> 00:00:09,240
is we're going to look at the recursive
types when we declared

3
00:00:09,240 --> 00:00:13,920
really looked at type synonyms we tried
to declare

4
00:00:13,920 --> 00:00:17,449
a recursive types in an but we notice
that

5
00:00:17,449 --> 00:00:20,779
that didn't work and then I explained
that

6
00:00:20,779 --> 00:00:24,680
when you want to grade the recursive
died it has to go

7
00:00:24,680 --> 00:00:27,720
the a nominal type and what we're going
to do

8
00:00:27,720 --> 00:00:32,029
in this part of the lecture is we're
going to look at

9
00:00:32,029 --> 00:00:35,940
a few recursive and

10
00:00:35,940 --> 00:00:39,530
and the rigors have died that we're
going to look at

11
00:00:39,530 --> 00:00:43,649
first is did type of natural numbers

12
00:00:43,649 --> 00:00:47,180
of integers if you recall an

13
00:00:47,180 --> 00:00:51,140
the lecture on recursive functions what
we did

14
00:00:51,140 --> 00:00:55,960
there when we define the function by
every Kors and function over integers

15
00:00:55,960 --> 00:00:59,640
we sat well an integer can be either 0

16
00:00:59,640 --> 00:01:05,400
or it could be are the successor of an
integer and since we don't have

17
00:01:05,400 --> 00:01:08,470
and plus que patterns any more national
we would add to ride

18
00:01:08,470 --> 00:01:14,060
and -1 on the right hand side but if we
re percent

19
00:01:14,060 --> 00:01:17,860
integers in this way we can ride

20
00:01:17,860 --> 00:01:21,270
nyse: recursive functions on these two
cases

21
00:01:21,270 --> 00:01:25,460
its either 0 are the success are of a
natural number

22
00:01:25,460 --> 00:01:29,670
alright so natural number is either 0

23
00:01:29,670 --> 00:01:32,710
or Israel one more then

24
00:01:32,710 --> 00:01:36,240
another natural number and if you look
at the

25
00:01:36,240 --> 00:01:41,560
types of the constructors 0 is a
function that takes no arguments and

26
00:01:41,560 --> 00:01:43,140
returns a natural number

27
00:01:43,140 --> 00:01:47,119
and sock is a function addiction natural
number

28
00:01:47,119 --> 00:01:51,649
an returns another natural number that's
the dive she see their

29
00:01:51,649 --> 00:01:56,520
on the bottom

30
00:01:56,520 --> 00:01:59,439
okay so if we look

31
00:01:59,439 --> 00:02:03,450
add all the values of this type sock

32
00:02:03,450 --> 00:02:07,759
you will see that it starts at 0 dats
the base case then we have circled here

33
00:02:07,759 --> 00:02:09,590
on Circus Circus 0

34
00:02:09,590 --> 00:02:16,040
et cetera I mentioned before that we're
gonna glossing over

35
00:02:16,040 --> 00:02:20,640
certain details I'm here biggest one of
the values

36
00:02:20,640 --> 00:02:24,040
that a we can also have is

37
00:02:24,040 --> 00:02:28,420
undefined but since word you know Justin
introductory

38
00:02:28,420 --> 00:02:32,579
course I'm not going to talk about it
undefined and bottom

39
00:02:32,579 --> 00:02:35,810
so for now yeah I definitely its

40
00:02:35,810 --> 00:02:39,290
perfectly safe to do and this is there
gonna be a

41
00:02:39,290 --> 00:02:42,750
infinite Sat of values and died

42
00:02:42,750 --> 00:02:47,720
an net and

43
00:02:47,720 --> 00:02:50,959
as I said these

44
00:02:50,959 --> 00:02:54,000
this regard have died 3 percent

45
00:02:54,000 --> 00:02:58,109
numbers and what we can do as we can
take an instance

46
00:02:58,109 --> 00:03:02,579
of and this Nat type and map it

47
00:03:02,579 --> 00:03:07,260
to an integer an and the way we do that
this weekend

48
00:03:07,260 --> 00:03:11,660
turn every occurrence of the suck
constructor into one

49
00:03:11,660 --> 00:03:15,519
and every occurs %uh 0 in 20

50
00:03:15,519 --> 00:03:19,329
you see that we made day in the same
structure

51
00:03:19,329 --> 00:03:24,069
and we at da shop and we get 3 so what
we can do

52
00:03:24,069 --> 00:03:27,650
SEC did this is a home a morphism from

53
00:03:27,650 --> 00:03:30,919
NAT two integers an

54
00:03:30,919 --> 00:03:34,079
we can define that just like redefined
for

55
00:03:34,079 --> 00:03:37,669
are over lists we can define this
function

56
00:03:37,669 --> 00:03:40,739
using fold are over natural numbers

57
00:03:40,739 --> 00:03:44,200
an for now

58
00:03:44,200 --> 00:03:48,000
we're going to do is recursively show
here is a function that goes from

59
00:03:48,000 --> 00:03:52,829
net to ent so nets to end of 0 is 0

60
00:03:52,829 --> 00:03:56,150
and Nat of end of and blush long

61
00:03:56,150 --> 00:03:59,269
is net

62
00:03:59,269 --> 00:04:02,569
of the end of an plus one

63
00:04:02,569 --> 00:04:06,450
and we can go the other way around every
get an integer

64
00:04:06,450 --> 00:04:09,900
we can get a natural number 0

65
00:04:09,900 --> 00:04:13,019
become 0 and here you see

66
00:04:13,019 --> 00:04:17,669
where I miss and plus que patterns and
becomes the sock

67
00:04:17,669 --> 00:04:22,720
of and and -1 it would be not much nicer
if this would be

68
00:04:22,720 --> 00:04:26,300
and blush wrong is this Aug of and do
not

69
00:04:26,300 --> 00:04:29,330
of but ya we have two

70
00:04:29,330 --> 00:04:32,639
respected the decisions that has school

71
00:04:32,639 --> 00:04:36,020
an Kurt Haskell committee makes

72
00:04:36,020 --> 00:04:39,780
K now what you can do is you can try to
prove

73
00:04:39,780 --> 00:04:44,470
that these functions are in versus and
then you can show that NAT

74
00:04:44,470 --> 00:04:48,290
is isomorphic to and and

75
00:04:48,290 --> 00:04:52,500
and of course a.m. you now we're
shoveling the fact that there's

76
00:04:52,500 --> 00:04:59,500
bottoms involved here under the carpet
given to Naturals weekend

77
00:04:59,680 --> 00:05:03,419
add them up by first converting them to
integers

78
00:05:03,419 --> 00:05:06,960
and then converting them back to nets

79
00:05:06,960 --> 00:05:10,610
a thats

80
00:05:10,610 --> 00:05:13,919
carry our really brute force ride

81
00:05:13,919 --> 00:05:17,320
so what we have these natural numbers

82
00:05:17,320 --> 00:05:21,850
we're going to convert them to integers
add them up and then conferred a result

83
00:05:21,850 --> 00:05:22,350
back

84
00:05:22,350 --> 00:05:27,060
I'll we take and natural number
converted to an integer

85
00:05:27,060 --> 00:05:30,410
take the other one over to do to ensure
at them up

86
00:05:30,410 --> 00:05:35,010
convert it back that's not very
efficient so instead

87
00:05:35,010 --> 00:05:38,010
we can t find this directly

88
00:05:38,010 --> 00:05:41,630
by induction over the natural numbers
show if we

89
00:05:41,630 --> 00:05:44,800
at 02 an that's the same as an

90
00:05:44,800 --> 00:05:48,729
and every at am blessed long to an

91
00:05:48,729 --> 00:05:52,780
well that this am plus an blush well

92
00:05:52,780 --> 00:05:56,190
and that's their definition that you see

93
00:05:56,190 --> 00:06:00,780
here so I think this wrong is much more
elegant

94
00:06:00,780 --> 00:06:03,910
and this rom but yeah they are

95
00:06:03,910 --> 00:06:08,010
equivalent if we

96
00:06:08,010 --> 00:06:12,150
am executes an example so we want to add

97
00:06:12,150 --> 00:06:13,670
to

98
00:06:13,670 --> 00:06:16,270
tu wong at:

99
00:06:16,270 --> 00:06:19,450
an we recursively

100
00:06:19,450 --> 00:06:22,810
bush the addition inside and

101
00:06:22,810 --> 00:06:27,110
take Wong of the sex outside

102
00:06:27,110 --> 00:06:31,530
we do that several times she see that
the ad gets push push push

103
00:06:31,530 --> 00:06:35,050
insights an until it hits the

104
00:06:35,050 --> 00:06:38,210
0 and that's here all and their ego

105
00:06:38,210 --> 00:06:41,470
the if we add to lush lawn

106
00:06:41,470 --> 00:06:44,670
we get 3 great

107
00:06:44,670 --> 00:06:49,100
so that was the end of Part two

108
00:06:49,100 --> 00:06:52,600
and I'll see you in a few minutes

109
00:06:52,600 --> 00:06:54,560
we're going to talk about type class