£ сс

(+1) . fold (+) 0= fold (+) 1

Теперь уравнение можно преобразовать с использованием свойства объединения. Получаем, что уравнение следует из следующих двух предположений:

(+1) 0= 1

(+1) ((+) x y)= (+) x ((+1) y)

Упрощение этих уравнений, пользуясь определением и секционированием, даёт, 0 + 1 = 1 и (x + y) + 1 = x + (y + 1). Полученные равенства являются арифметически верными. В более обобщённом виде добавляем в этом примере произвольный инфиксный оператор Ф, который является ассоциативным. Применив свойство объединения, получаем, что:

(Ф a) . fold (Ф) b= fold (Ф) (b Ф a)

Более интересным примером является следующее хорошо известное уравнение, которое показывает, что оператор map использует композицию (.):

map f . map g= map (f . g)

Заменяя второе и третье вхождение оператора map в уравнении его определением с использованием свёртки, получаем, что равенство может быть переписано в виде, подходящем для применения свойства объединения:

map f . fold (\x xs -> g x : xs) [] fold (\x xs -> (f . g) x : xs) []

Обращаясь к свойству объединения, упрощаем. Получаем следующие два уравнения, которые являются верными по определению map и (.):

map f []= []

map f (g x : y) = (f . g) x : map f y

В дополнение к вышеупомянутым особенностям, есть множество других полезных свойств оператора свёртки, которые могут быть получены при помощи свойства универсальности оператора свёртки (Bird, 1998). Однако, свойство объединения применяется в большинстве практических случаев, и всегда может быть приведено к свойству универсальности, если его невозможно применить.

3.3. Универсальность как способ определения

Будучи используемым в качестве принципа доказательства, универсальное свойство оператора свёртки может быть использовано как способ определения, который ведёт преобразование рекурсивных функций в соответствии с определением, используя свёртку. В качестве примера рассмотрим рекурсивно определенную функцию sum, которая вычисляет сумму списка чисел:

£ то

sum sum [] sum (x:xs)

[Int] -> Int 0

x + sum xs

Предположим теперь, что мы хотим переопределить эту функцию, используя свёртку. Таким образом, мы хотим решить уравнение sum = fold f v для функции f и значения v. Заметим, что уравнение соответствует правой части универсального свойства оператора свёртки. Отсюда получаем, что уравнение эквивалентно следующим двум равенствам:

sum [] sum (x:xs)

f x (sum xs)

С использованием первого уравнения и определения sum, сразу же получаем, что v = 0. Из второго уравнения мы вычисляем определение дляf следующим образом:

sum (x:xs) x + sum xs x + y

f x (sum xs) f x (sum xs) f x y

Пользуясь универсальностью оператора свёртки, получаем:

sum= fold (+) 0

Отметим, что ключевым моментом в вычислении определения для f является обобщение выражения sum xs для новой переменной y. Фактически, такой шаг обобщения не является специфичным для функции sum, но этот шаг будет ключевым в преобразовании какой-либо рекурсивной функции из определения с использованием оператора свёртки.

Конечно, пример с функцией sum - достаточно искусственный, потому что её определение непосредственно использует оператор свёртки. Однако, есть много примеров функций, чьё определение использует свёртку не настолько явно. Например, рассмотрим рекурсивно определенную функцию mapf которая применяет функцию f к каждому элементу списка:

map f []=

map f (x:xs) =

(a -> b) -> ([a] -> [b]) []

f x : map f xs

Для переопределения функции mapf использующей свёртку, мы должны решить уравнение mapf=foldg v для функции g и значения v. Используя универсальность оператора свёртки, получаем, что это уравнение эквивалентно следующим двум уравнениям:

map f []=

map f (x:xs) =

g x (map f xs)

Из первого уравнения по определению функции map непосредственно получаем, что v = []. По второму уравнению, вычисляем определение для g следующим образом:

map f (x:xs)=g x (mapfxs)

f x : map f xs=g x (mapfxs)

f x : ys=g x ys

g=\x ys ->fx :ys

Таким образом, с использованием универсальности оператора свёртки, мы вычислили что:

map f= fold (\x ys -> f x : ys) []

Вообще, любая функция, работающая со списками, и которая может быть выражена с использованием оператора свёртки, может быть преобразована к такому виду при помощи свойства универсальности оператора свёртки.