如何解释笛卡尔积实现中foldr的递归到高阶函数等价转换？

Great question! Let's break down this equivalence step by step, using the definition of foldr and inductive reasoning to make the connection crystal clear.

First, let's restate both function definitions for reference:

Recursive h Definition #

h [] xss = []
h (x : xs) xss = foldr f (h xs xss) xss
  where f xs ys = (x: xs) : ys

Foldr-Based h'' Definition #

h'' xs xss = foldr g [] xs
  where g x zss = foldr f zss xss
        f xs ys = (x : xs) : ys

Step 1: Base Case (Empty List xs = []) #

Start with the simplest scenario where xs is empty:

• For h: h [] xss = [] (directly from its recursive definition)
• For h'': h'' [] xss = foldr g [] [] = [] (since foldr returns the initial value when given an empty input list)

They match perfectly here.

Step 2: Inductive Step (Non-Empty List xs = x : xs') #

We use inductive reasoning here—assume that for some list xs', h xs' xss = h'' xs' xss (this is our inductive hypothesis). We need to prove h (x : xs') xss = h'' (x : xs') xss.

Expand h (x : xs') xss #

From the recursive definition of h:

h (x : xs') xss = foldr f (h xs' xss) xss

Substitute h xs' xss with h'' xs' xss (per our inductive hypothesis):

= foldr f (h'' xs' xss) xss

Expand h'' (x : xs') xss #

Using the core definition of foldr:

h'' (x : xs') xss = g x (h'' xs' xss)

But g x zss is defined as foldr f zss xss, so substitute that in:

= foldr f (h'' xs' xss) xss

This is exactly the same expression we got for h (x : xs') xss! So if the functions are equal for xs', they're equal for x : xs' too.

Step 3: Intuitive Example with a Concrete List #

Let's use xs = [x1, x2] to see how both functions expand to identical results:

Expanding h [x1, x2] xss #

h [x1, x2] xss = foldr f (h [x2] xss) xss
= foldr f (foldr f (h [] xss) xss) xss
= foldr f (foldr f [] xss) xss

Expanding h'' [x1, x2] xss #

h'' [x1, x2] xss = g x1 (g x2 [])
= foldr f (g x2 []) xss
= foldr f (foldr f [] xss) xss

Same exact output! The recursive h builds nested foldr calls by processing each element of xs one by one, while h'' uses foldr to wrap each element's transformation (the g x function, itself a foldr) into a single pass over xs.

What's g Actually Doing? #

To make it even more intuitive:

• g x zss takes a list zss, prepends every element of xss with x, then appends that entire collection to zss (thanks to foldr f zss xss, where f xs ys = (x:xs):ys).
• The recursive h does this by first processing the tail of xs to get h xs xss, then applying this "prepend x to all xss elements" operation and combining it with the tail result.
• h'' uses foldr to chain these "prepend x" operations starting from an empty list—this is exactly the same as the recursive approach, just rephrased using higher-order foldr composition.

内容的提问来源于stack exchange，提问作者jiamo