Epb시�紅灯

It has only a list argument if you have already applied it to the natural number argument.

This is Haskell notation where space applies a function to an argument.

I've heard that this jumping back and forth between applicative location with brackets and just application by juxtaposition as in Haskell is confusing to some.

It will be sort of hard to give up because otherwise I'll run into trouble with covering the blackboard in brackets.

There is a reason that Haskell writes application by juxtaposition.

But if there is anything unclear about this, ask me.

Well, as now actually of course.

So explicitly, yes.

It's a function that is described in number 2c in partially applied form.

So we have already applied it to a natural number argument n and what we get is a function that only expects a list argument.

And yes, so the recursion requires changing the parameter n as well.

But the recursion should be over the list, not over the natural number.

That's why it's written this way here.

In principle, you could do recursion over either of them.

So you could have the idea of doing the recursion over the natural numbers argument and this works fine for some time until you notice precisely the case that came up in the question just now.

If you do recursion over the natural number, then you need to do a case distinction at some point over whether the list is empty.

If you do recursion over the list argument, then basically that goes away because you're doing case distinction over that anyway.

So but yes, this is one of those cases basically where, so in that case maybe writing it that way is again somewhat unfortunate.

And so the fold, if you get this as a fold, then the type is really this.

So basically that reflects what I was just saying, right?

So the recursion is over this part, so that's what you get when you write a fold.

And the natural number argument is hidden here by currying.

So it is one of those currying exercises again, just now with arguments of different types.

So what's going to happen here of course is you change, I'll show you this shortly.

So in the recursive call here, you apply this function here, right?

And you apply it to the predecessor of the current argument.

So this sounds a bit like there would be a case distinction coming up on whether there is a predecessor or not, right?

So the current argument could be zero.

I mean feel free to describe the function that you apply the fold to in whichever way you like in this case, right?

So don't worry about it excessively about writing in point-free style.

So here's a hint to this.

So for this case at least, it's no problem at all to, I will not deem it a problem to write fold R of something and point-full,

because here there will be a slight issue about the zero.

Yes?

Yeah, the natural number is the first argument.

And the final idea to define is something like uncurrier of swap of take or something, right?

So in the end I have to fiddle with the arguments.

I mean write it this way, then the audio of the arguments is changed.

I mean basically that's what you do.

You encode primitive recursion in fold by basically currying,

and that's of course primitive recursion over the first argument only.

And if you want primitive recursion over another argument, say the second,

then you have to swap the arguments around before you curry basically.

So let me briefly think whether, I was wondering whether the case for zero is a proper case distinction

or whether we can just ignore it.

Well okay, so strictly speaking, if you want to write the function that you put here in a point-free manner,

this will again be a fold this time over the natural numbers, right,

which gives you your case distinction basically.

But like I said, so let's not overdo it in this case,