52700.fb2 Учебник по Haskell - читать онлайн бесплатно полную версию книги . Страница 271

Учебник по Haskell - читать онлайн бесплатно полную версию книги . Страница 271

Видите в типе и той и другой функции стоит требование о том, что f является функтором. Катаморфизм и

анаморфизм отображают объекты в стрелки. По типу функций fold и unfold мы можем сделать вывод, что

объектами в нашей категории будут стрелки вида

f a -> a

или для свёрток:

a -> f a

А стрелками будут обычные функции одного аргумента. Теперь дадим более формальное определение.

Эндофунктор F : A → A определяет стрелки α : F A → A, которые называется F - алгебрами. Стрелку

h : A → B называют F - гомоморфизмом, если следующая диаграмма коммутирует:

F A

α

A

F h

h

F B

B

β

Или можно сказать по другому, для F -алгебр α : F A → A и β : F B → B выполняется:

F h ; β = α ; h

Это свойство совпадает со свойством естественного преобразования только вместо одного из функторов

мы подставили тождественный функтор I. Определим категорию Alg( F ), для категории A и эндофунктора

F : A → A

• Объектами являются F -алгебры F A → A, где A – объект категории A

• Два объекта α : F A → A и β : F B → B соединяет F -гомоморфизм h : A → B. Это такая стрелка из

A, для которой выполняется:

F h ; β = α ; h

• Композиция и тождественная стрелка взяты из категории A.

Если в этой категории есть начальный объект inF : F T → T , то определён катаморфизм, который

переводит объекты F A → A в стрелки T → A. Причём следующая диаграмма коммутирует:

in

F T

F

T

F ( | α |)

( | α |)

F A

A

α

Этот катаморфизм и будет функцией свёртки для рекурсивного типа . Понятие Alg( F ) можно перевернуть

и получить категорию CoAlg( F ).

244 | Глава 16: Категориальные типы

• Объектами являются F -коалгебры A → F A, где A – объект категории A

• Два объекта α : F A → A и β : F B → B соединяет F -когомоморфизм h : A → B. Это такая стрелка

из A, для которой выполняется:

h ; α = β ; F h

• Композиция и тождественная стрелка взяты из категории A.

Если в этой категории есть конечный объект, его называют outF : T → F T , то определён анаморфизм,

который переводит объекты A → F A в стрелки A → T .

Причём следующая диаграмма коммутирует:

in