Объясните, пожалуйста, на самом простом языке без жаргона универсальное свойство fold?

(Режим жаргона выключен :-)

Универсальное свойство — это всего лишь способ доказать, что два выражения равны. (Это то, что на жаргоне означает «принцип доказательства».) Универсальное свойство гласит, что если вы можете доказать эти два уравнения

g []     = v
g (x:xs) = f x (g xs)

то вы можете заключить дополнительное уравнение

g = fold f v

Верно и обратное, но это легко показать, просто расширив определение fold. Универсальное свойство — это гораздо более глубокое свойство (это жаргонный способ сказать, что менее очевидно, почему оно истинно).

Причина, по которой это вообще интересно, заключается в том, что это позволяет вам избежать доказательства по индукции, чего почти всегда стоит избегать.

статья определяет два свойства:

g   []     = v
g (x : xs) = f x (g xs)

а затем заявляет, что fold — это не только функция, удовлетворяющая этим свойствам, но и единственная функция, удовлетворяющая этим свойствам. то, что он уникален в этом отношении, делает его «универсальным» в том смысле, в котором он используется в статье.

Свойство fold состоит в том, что это функция рекурсии списка, которая эквивалентна всем другим функциям рекурсии списка, если вы зададите ей правильные параметры.

У него есть это свойство, потому что он принимает в качестве параметра функции, которые будут применяться к элементам в списке.

Например, если мы написали простую функцию суммирования:

sum []          = 0
sum (head:tail) = head + (sum tail)

тогда мы могли бы вместо этого написать это как функцию fold, передав оператор (+), который мы хотим использовать для объединения элементов:

sum list = foldl (+) 0 list

Таким образом, любая функция, которая просто и рекурсивно работает со списком, может быть переписана как функция свертки. Эта эквивалентность является свойством, которым она обладает. Я полагаю, что он называет это свойство универсальным, потому что оно работает для всех этих линейно-списочно-рекурсивных алгоритмов без исключения.

И, как он объясняет, причина, по которой это свойство так полезно, заключается в том, что, поскольку мы можем показать, что все эти другие алгоритмы на самом деле эквивалентны свертыванию, доказывая что-то о свертывании, мы также доказываем это для всех других алгоритмов.

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

-- forall - A kind of for next loop
-- list is list of things to loop through
-- f is function to perform on each thing
-- c is the function which combines the results of f
-- e is the thing to combine to when the end of the list is reached
forall :: [a] -> (a->b) -> (b->b->b) -> b -> b
forall [] f c e = e
forall (x:xs) f c e = c (f x) (forall xs f c e)

(На самом деле это немного мощнее, чем foldl, потому что у него есть дополнительная функция применения функции f к каждому элементу в списке.)

Ну никто ничего не доказал о моей функции. Но это не имеет значения, потому что я могу показать, что моя функция на самом деле является функцией fold:

forall l f c e = foldl c e (map fn l)

И, следовательно, все, что было доказано в отношении fold, также подтверждается для моей функции forall и всех ее применений в моей программе. (Обратите внимание, что нам даже не нужно рассматривать, какая функция c предоставляется в каждом из различных вызовов forall и foldl, это не имеет значения!)

Я только что нашел новую (для меня) запись в Википедии «Универсальная собственность». Это проливает тонну света на этот вопрос. Вот ссылка: Из нее я (условно) делаю следующие выводы:

1. Хотя вы можете придумать 100 различных способов обхода списка, попутных вычислений и получения одного конечного значения из списка, все 100 из этих способов являются изоморфными (это означает, что в конечном итоге они одинаковый). На самом деле есть только один способ уменьшить список до одного значения, и это FOLD.
2. Fold также является «наиболее эффективным решением» для сокращения списка до одного значения. Или, можно сказать, самое «факторизованное» или самое «упрощенное» решение.

Кажется, что вместе эти два пункта отражают значение термина «универсальное свойство».

Хотя это может быть немного сложно понять, не читая предыдущие посты в серии, объясняющие универсальные свойства с категориальной точки зрения, этот пост дает подробное категориальное объяснение универсального свойства fold, а также map и filter.

http://jeremykun.com/2013/09/30/the-universal-properties-of-map-fold-and-filter/

Хотя я еще не написал его, продолжение обобщит это (и сделает его намного проще для понимания, хотя и более абстрактным) для «складчатых» операций над общими структурами данных.

Подробнее о том, что такое универсальное свойство, см. в этом сообщении: http://jeremykun.com/2013/05/24/universal-properties/

А здесь ссылки на все посты из серии: http://jeremykun.com/main-content/

По правде говоря, принятый в настоящее время ответ — это самый простой способ понять, что универсальное свойство говорит о свертывании. Статьи, указанные выше, просто дают более подробное техническое описание с помощью теории категорий, которое отсутствует в рассматриваемой статье. Однако я не согласен с утверждением в принятом ответе, что универсальное свойство является гораздо более глубоким свойством, чем утверждение без жаргона. Универсальное свойство сворачивания — это точно такое же утверждение, только упакованное в язык начальных и конечных объектов в соответствии с характером анализа вещей с помощью теории категорий. Этот анализ ценен именно своими естественными обобщениями.