In short: the foldr produces a function (not a list of values), and that function will then generate that list.
Let us first ignore the foldr for a while, and concentrate on the function used in the foldr, let us call this function eval:
eval x g i = seq i (f i x (g (i+1))))
We will ignore the seq here: yes it has some semantics: evaluating (to weak head normal form) the i and checking if i is bottom, but let us assume that this will not introduce a bottom. So eval is - more or less - equivalent to:
eval x g i = f i x (g (i+1))
Now we can take the foldr context back into account:
ifoldr f = foldr eval (const z) xs 0
where eval x g i = f i x (g (i+1))
Now foldr is defined (for lists, but let us keep things simple here), as:
foldr _ z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
For a list with three elements [x1, x2, x3], this thus means that:
foldr eval (const z) [x1, x2, x3]
looks like:
-- foldr eval (const z) [x1, x2, x3] is equivalent to
eval x1 (eval x2 (eval x3 (const z)))
Since eval is defined as above, that means that we can specialize it to:
\i1 -> f i1 x1 ((\i2 -> f i2 x2 (\i3 -> f i3 x3 (const z)) (i2 + 1)) (i1 + 1))
Or perhaps in a way that makes the structure more clear:
\i1 -> (
f i1 x1
\i2 -> (
f i2 x2
\i3 -> (
f i3 x3
(const z) (i3+1)
) (i2+1)
) (i1+1)
)
So as you can see the outer function takes a parameter (here i1), and makes a call to f with i1 (the index), x1 (the first item), and as last item the result of a call that is the "fold" of the remaining list. We thus make a call with i2 as parameter, but that i2 is bound with i1+1.
So if we perform substitution (substuting i3 with i2 + 1), which is how lambda calculus works, we obtain:
\i1 -> (
f i1 x1
\i2 -> (
f i2 x2
(
f (i2+1) x3
(const z) (i2+1+1)
)
) (i1+1)
)
and furthermore we can substitute i2 with i1+1:
\i1 -> (
f i1 x1
(
f (i1+1) x2
(
f (i2+1) x3
(const z) (i1+1+1+1)
)
)
Since (const z) maps to z, regardless what the parameter is, we can substitute (const z) (i1+1+1+1) with z, so:
\i1 -> (
f i1 x1
(
f (i1+1) x2
(
f (i1+1+1) x3
z
)
)
So now we know what foldr eval (const z) [x1, x2, x3] maps to, but there is a final fuction application: the 0 at the end.
So that means that we make a call to the above defined lambda-expression with 0, so this collapses to:
\i1 -> (
f i1 x1
(
f (i1+1) x2
(
f (i1+1+1) x3
z
)
) 0
and thus:
(
f 0 x1
(
f (0+1) x2
(
f (0+1+1) x3
z
)
)
or in a compact form:
(f 0 x1 (f 1 x2 (f 2 x3 z)))
So we managed to inject indices in our solution.
Now the seq of course has a function: it will prevent making huge (left-recursive) expression trees for the index, instead of ((((1+1)+1)+1)+1)+1, it will ensure that each time we increment it, it is immediately evaluated, so that we will never obtain 1+1+1, but always 2+1, and immidiately resolve it to 3.
