"通过将所需结果与参数列表配对而定义的有限列表上的任何函数总是可以根据折叠重新定义"

Question

我正在阅读论文关于折叠的普遍性和表现力的教程,并且我坚持关于生成元组的部分.在展示了如何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           = ([], [])

该文件指出:

实际上,这个结果是一个通用定理的实例(Meertens,1992),它指出通过将所需结果与参数列表配对而定义的有限列表上的任何函数总是可以用折叠重新定义,尽管并不总是在一种不利用函数的原始(可能是递归)定义的方法.

我看了Meerten的论文,但没有背景(类别理论？类型理论？),并没有找到如何证明这一点.

有一个相对简单的"证据"为什么会这样？或者只是一个简单的解释,为什么我们可以在折叠方面重新定义有限列表上的所有函数,如果我们将结果与原始列表配对.

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 []), [])

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