泛化 fold 使其具有足够的表现力来定义任何有限递归？
Generalizing fold such that it becomes expressive enough to define any finite recursion?
所以，有一个被称为 "universal property of fold" 的东西，其内容如下：
g [] = i; g (x:xs) = f x (g xs) <=> g = fold f i
但是，正如您现在可能的那样，很少有像 dropWhile 这样的情况，不能将其重新定义为 fold f i ，除非您将其概括化。
最简单但明显的概括方法是重新定义通用 属性:
g' y [] = j y; g' y (x:xs) = h y x xs (g' y xs) <=> g' y = fold (?) l
在这一点上我可以做出我的假设：我假设存在某种函数p :: a -> b -> b，它将满足方程g' y = fold p l。让我们尝试在通用 属性 的帮助下求解给定的方程，在最开始提到：
g' y [] = j y = fold p l [] = l => j y = lg' y (x:xs) = h y x xs (g' y xs) = fold p l (x:xs) = p x (fold p l xs) = p x (g' y xs) => 让 rs = (g' y xs), h y x xs rs = p x rs, 这是错误的: xs 从左边自由出现并且因此平等不能成立。
现在让我尝试解释我得出的结果并提出问题。
我看到问题是 xs emerging as unbound variable;对于各种情况都是如此，包括上面提到的 dropWhile。这是否意味着解方程的唯一方法是 "extending" rs 对一对 (rs, xs)？换句话说，fold累积成元组而不是单一类型（忽略元组本身是单一类型的事实）？有没有其他方法可以概括绕过配对？
正如你所说。通用 属性 表示 g [] = i; g (x:xs) = f x (g xs) 当且仅当 g = fold f i。这不适用于 dropWhile 的直接定义，因为 would-be f :: a -> [a] -> [a] 不仅取决于当前折叠步骤的元素和累加值，还取决于整个列表后缀留待处理（用你的话来说，“xs emerg[es] 作为未绑定变量”）。可以做的是扭曲 dropWhile，这样对列表后缀的这种依赖性就可以通过元组在累加值中体现出来——cf。 dropWhilePair from this question, with f :: a -> ([a], [a]) -> ([a], [a]) -- or a function -- as in ...
dropWhileFun = foldr (\x k -> \p -> if p x then k p else x : k (const False)) (const [])
... 与 f :: a -> ((a -> Bool) -> [a]) -> ((a -> Bool) -> [a]).
归根结底，普遍的 属性 就是它的本质——关于 foldr 的一个基本事实。并非所有递归函数都可以立即通过 foldr 表达，这绝非偶然。事实上，你的问题给 table 带来的元组解决方法直接反映了同构的概念（有关它们的解释，请参见 What are paramorphisms? and its exquisite answer by Conor McBride). At face value, paramorphisms are generalisations of catamorphisms (i.e. a straightforward fold); however, it only takes a slight contortion to implement paramorphisms in terms of catamorphisms. (Additional technical commentary on that might be found, for instance, in Chapter 3 of Categorical Programming With Inductive and Coinductive Types, Varmo Vene's PhD thesis。）
所以，有一个被称为 "universal property of fold" 的东西，其内容如下：
g [] = i; g (x:xs) = f x (g xs) <=> g = fold f i
但是，正如您现在可能的那样，很少有像 dropWhile 这样的情况，不能将其重新定义为 fold f i ，除非您将其概括化。
最简单但明显的概括方法是重新定义通用 属性:
g' y [] = j y; g' y (x:xs) = h y x xs (g' y xs) <=> g' y = fold (?) l
在这一点上我可以做出我的假设：我假设存在某种函数p :: a -> b -> b，它将满足方程g' y = fold p l。让我们尝试在通用 属性 的帮助下求解给定的方程，在最开始提到：
g' y [] = j y = fold p l [] = l=>j y = lg' y (x:xs) = h y x xs (g' y xs) = fold p l (x:xs) = p x (fold p l xs) = p x (g' y xs)=> 让rs = (g' y xs),h y x xs rs = p x rs, 这是错误的:xs从左边自由出现并且因此平等不能成立。
现在让我尝试解释我得出的结果并提出问题。
我看到问题是 xs emerging as unbound variable;对于各种情况都是如此，包括上面提到的 dropWhile。这是否意味着解方程的唯一方法是 "extending" rs 对一对 (rs, xs)？换句话说，fold累积成元组而不是单一类型（忽略元组本身是单一类型的事实）？有没有其他方法可以概括绕过配对？
正如你所说。通用 属性 表示 g [] = i; g (x:xs) = f x (g xs) 当且仅当 g = fold f i。这不适用于 dropWhile 的直接定义，因为 would-be f :: a -> [a] -> [a] 不仅取决于当前折叠步骤的元素和累加值，还取决于整个列表后缀留待处理（用你的话来说，“xs emerg[es] 作为未绑定变量”）。可以做的是扭曲 dropWhile，这样对列表后缀的这种依赖性就可以通过元组在累加值中体现出来——cf。 dropWhilePair from this question, with f :: a -> ([a], [a]) -> ([a], [a]) -- or a function -- as in
dropWhileFun = foldr (\x k -> \p -> if p x then k p else x : k (const False)) (const [])
... 与 f :: a -> ((a -> Bool) -> [a]) -> ((a -> Bool) -> [a]).
归根结底，普遍的 属性 就是它的本质——关于 foldr 的一个基本事实。并非所有递归函数都可以立即通过 foldr 表达，这绝非偶然。事实上，你的问题给 table 带来的元组解决方法直接反映了同构的概念（有关它们的解释，请参见 What are paramorphisms? and its exquisite answer by Conor McBride). At face value, paramorphisms are generalisations of catamorphisms (i.e. a straightforward fold); however, it only takes a slight contortion to implement paramorphisms in terms of catamorphisms. (Additional technical commentary on that might be found, for instance, in Chapter 3 of Categorical Programming With Inductive and Coinductive Types, Varmo Vene's PhD thesis。）