"Любая функция в конечных списках, которая определяется путем спаривания желаемого результата с списком аргументов, всегда может быть переопределена в терминах fold"

Я читал статью учебник по универсальности и выразительность 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           = ([], [])

В документе говорится:

Фактически, этот результат является экземпляром (Meertens, 1992), в которой утверждается, что любая функция на конечных списках, определяемые путем объединения желаемого результата с списком аргументов, всегда можно переопределить в терминах складки, хотя и не всегда таким образом, чтобы не использовать оригинал (возможно, рекурсивного) определения для функции.

Я смотрел Meerten Paper, но не имел фона (теория теории категорий?) и не совсем понял, как это было доказано.

Существует ли относительно простое "доказательство", почему это так? Или просто простое объяснение того, почему мы можем переопределить все функции в конечных списках в терминах складки, если мы сопоставим результаты с исходным списком.

Ответы

Ответ 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 []), [])

EDIT: добавлен ~, после чего он работает и для бесконечных списков.