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
T
F
F T
[( α )]
F [( α )]
A
F A
α
Если для категории A и функтора F определены стрелки inF и outF , то они являются взаимнообратными
и определяют изоморфизм T ∼
= F T . Часто объект T в случае Alg( F ) обозначают µF , поскольку начальный
объект определяется функтором F , а в случае CoAlg( F ) обозначают νF .
Типы, которые являются начальными объектами, принято называть индуктивными, а типы, которые яв-
ляются конечными объектами – коиндуктивными.
Существование начальных и конечных объектов
Мы говорили, что если начальный(конечный) объект существует, а когда он существует? Рассмотрим
один важный случай. Если категория является категорией, в которой объектами являются полные частично
упорядоченные множества, а стрелками являются монотонные функции, такие категории называют CPO, и
функтор – полиномиальный, то начальный и конечный объекты существуют.
Полные частично упорядоченные множества
Оказывается на значениях можно ввести частичный порядок. Порядок называется частичным, если отно-
шение ≤ определено не для всех элементов, а лишь для некоторых из них. Частичный порядок на значениях
отражает степень неопределённости значения. Самый маленький объект это полностью неопределённое зна-
чение ⊥. Любое значение типа содержит больше определённости чем ⊥.
Для того чтобы не путать упорядочивание значений по степени определённости с обычным числовым
порядком, пользуются специальным символом . Запись
a
b
означает, что b более определено (или информативнее) чем a.
Так для логических значений определены два нетривиальных сравнения:
data Bool = T rue | F alse
⊥
T rue