welcome back an well we're going to do now
is we're going to look at the recursive types when we declared
really looked at type synonyms we tried to declare
a recursive types in an but we notice that
that didn't work and then I explained that
when you want to grade the recursive died it has to go
the a nominal type and what we're going to do
in this part of the lecture is we're going to look at
a few recursive and
and the rigors have died that we're going to look at
first is did type of natural numbers
of integers if you recall an
the lecture on recursive functions what we did
there when we define the function by every Kors and function over integers
we sat well an integer can be either 0
or it could be are the successor of an integer and since we don't have
and plus que patterns any more national we would add to ride
and -1 on the right hand side but if we re percent
integers in this way we can ride
nyse: recursive functions on these two cases
its either 0 are the success are of a natural number
alright so natural number is either 0
or Israel one more then
another natural number and if you look at the
types of the constructors 0 is a function that takes no arguments and
returns a natural number
and sock is a function addiction natural number
an returns another natural number that's the dive she see their
on the bottom
okay so if we look
add all the values of this type sock
you will see that it starts at 0 dats the base case then we have circled here
on Circus Circus 0
et cetera I mentioned before that we're gonna glossing over
certain details I'm here biggest one of the values
that a we can also have is
undefined but since word you know Justin introductory
course I'm not going to talk about it undefined and bottom
so for now yeah I definitely its
perfectly safe to do and this is there gonna be a
infinite Sat of values and died
an net and
as I said these
this regard have died 3 percent
numbers and what we can do as we can take an instance
of and this Nat type and map it
to an integer an and the way we do that this weekend
turn every occurrence of the suck constructor into one
and every occurs %uh 0 in 20
you see that we made day in the same structure
and we at da shop and we get 3 so what we can do
SEC did this is a home a morphism from
NAT two integers an
we can define that just like redefined for
are over lists we can define this function
using fold are over natural numbers
an for now
we're going to do is recursively show here is a function that goes from
net to ent so nets to end of 0 is 0
and Nat of end of and blush long
is net
of the end of an plus one
and we can go the other way around every get an integer
we can get a natural number 0
become 0 and here you see
where I miss and plus que patterns and becomes the sock
of and and -1 it would be not much nicer if this would be
and blush wrong is this Aug of and do not
of but ya we have two
respected the decisions that has school
an Kurt Haskell committee makes
K now what you can do is you can try to prove
that these functions are in versus and then you can show that NAT
is isomorphic to and and
and of course a.m. you now we're shoveling the fact that there's
bottoms involved here under the carpet given to Naturals weekend
add them up by first converting them to integers
and then converting them back to nets
a thats
carry our really brute force ride
so what we have these natural numbers
we're going to convert them to integers add them up and then conferred a result
back
I'll we take and natural number converted to an integer
take the other one over to do to ensure at them up
convert it back that's not very efficient so instead
we can t find this directly
by induction over the natural numbers show if we
at 02 an that's the same as an
and every at am blessed long to an
well that this am plus an blush well
and that's their definition that you see
here so I think this wrong is much more elegant
and this rom but yeah they are
equivalent if we
am executes an example so we want to add
to
tu wong at:
an we recursively
bush the addition inside and
take Wong of the sex outside
we do that several times she see that the ad gets push push push
insights an until it hits the
0 and that's here all and their ego
the if we add to lush lawn
we get 3 great
so that was the end of Part two
and I'll see you in a few minutes
we're going to talk about type class