haskell - "Any function on finite lists that is defined by pairing the desired result with the argument list can always be redefined in terms of fold"

Question

我正在阅读论文A tutorial on the universality andexpressiveness of fold ，并停留在关于生成元组的部分。显示后如何正常定义dropWhile不能用折叠来定义，例如定义 dropWhile证明了使用元组:

dropWhile :: (a -> Bool) -> [a] -> [a]
dropWhile p = fst . (dropWhilePair p)

dropWhilePair :: (a -> Bool) -> [a] -> ([a], [a])
dropWhilePair p = foldr f v
  where
    f x (ys,xs) = (if p x then ys else x : xs, x : xs)
    v           = ([], [])

该论文指出:

In fact, this result is an instance of a general theorem (Meertens, 1992) that states that any function on finite lists that is defined by pairing the desired result with the argument list can always be redefined in terms of fold, although not always in a way that does not make use of the original (possibly recursive) definition for the function.

我看了 Meerten's Paper但没有背景(范畴论？类型论？)，也不太明白这是怎么证明的。

有没有一个相对简单的“证明”为什么会这样？或者只是一个简单的解释，如果我们将结果与原始列表配对，为什么我们可以根据折叠重新定义有限列表上的所有函数。

Answer 1

鉴于您可以/可能需要在内部使用原始功能的说法，您的问题中所述的主张对我来说似乎微不足道:

rewriteAsFold :: ([a] -> (b, [a])) -> [a] -> (b, [a])
rewriteAsFold g = foldr f v where
    f x ~(ys,xs) = (fst (g (x:xs)), x:xs)
    v            = (fst (g []), [])

编辑:添加了 ~ ，之后它似乎也适用于无限列表。