This is the definition of list foldr
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr _ z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
In both foldl and foldr in the OP the n variable in lambda functions would seem to be for the accumulator, hence, I assume the n is considered the free variable? And then the wildcard in each lambda function refers to the bound variable, i.e., the list argument's elements to be folded. So I can recreate
foldr (+) 5 [1,2,3,4]
with
foldr (\x n -> x + n) 5 [1,2,3,4]
They both return 15. The first one results in
(+) 1 ((+) 2 ((+) 3 ((+) 4 5)))
but the second example I'm not sure how the (\x n -> x + n) is being applied in the form . . . f x (foldr f z xs) It obviously must be doing the same (+) 1 ((+) 2 ((+) 3 ((+) 4 5))) but how the function is being applied I don't understand. Beta reduction doesn't get me very far
\x n -> x + n (5)([1,2,3,4])
\x 5 -> x + 5 ([1,2,3,4])
but obviously the enclosing lambda calc for foldr is doing something to create the (+) 1 ((+) 2 ((+) 3 ((+) 4 5))) form.
BTW, is the t a format in
:type foldr
foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
something from category theory, i.e., for the list instance, t a is [a] What is the algebraic syntax where t a becomes [a] in the case of lists? It would be nice to understand some day exactly what :i Foldable is saying