笛卡尔积中的转换文件夹很难理解

Question

我跟着On Barron and Strachey's cartesian product function了解高阶函数的组合

我得到了一个重要的转换，我认为它不容易直接理解：

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

等于：

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

连我都得到了这些帮手：

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z [] = z
foldr f z (a:as) = f a (foldr f z as) 

-- change the name
h' :: (a -> b -> b) -> b -> [a] -> b
h' f z [] = z
h' f z (a:as) = f a (h' f z as)

所以我的问题是：解释转换容易吗？

Answer 1

本质上它归结为 h 是 xs 上的递归函数，而 foldr 概括了列表上的递归。请注意 h 如何在尾部 xs 上调用自己，就像 foldr 在尾部 as.

上调用自己一样

通过对ws的归纳，证明h ws xss = h'' ws xss。归纳推理，有两种情况需要考虑。

基本案例、ws = []

h [] xss = []  -- by definition of h

h'' [] xss
= foldr g [] xss  -- by definition of h''
= []              -- by definition of foldr

归纳步骤，ws = x : xs，假设h xs xss = h'' xs xss（归纳假设）

h (x : xs) xss
= foldr f (h xs xss) xss    -- by definition of h (N.B. f depends on x)
= foldr f (h'' xs xss) xss  -- by induction hypothesis
= g x (h'' xs xss)          -- by definition of g (N.B. g depends on xss)
= g x (foldr g [] xs)       -- by definition of h''
= foldr g [] (x : xs)       -- by definition of foldr
= h'' (x : xs) xss          -- by definition of h''

Answer 2

首先创建一个不带第二个参数的内部函数 xss，仅执行标准列表递归：

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

  -->

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

然后让我们看看我们如何用另一个作用于x的辅助函数和递归调用结果h' xs抽象出h'中的递归模式：

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

如果我们不想在 h' 中显式写出列表递归，这就是我们将传递给 foldr 的辅助函数：

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

笛卡尔积中的转换文件夹很难理解

It is hard to understand to a transform foldr in cartesian product

lambda

haskell

functional-programming

cartesian-product

fold