Учебник по Haskell

16.2 Индуктивные и коиндуктивные типы

С точки зрения теории категорий функция свёртки является катаморфизмом, а функция развёртки – ана-

морфизмом. Напомню, что катаморфизм – это функция которая ставит в соответствие объектам категории

с начальным объектом стрелки, которые начинаются из начального объекта, а заканчиваются в данном объ-

екте. Анаморфизм – это перевёрнутый наизнанку катаморфизм.

Начальным и конечным объектом будет рекурсивный тип. Вспомним тип свёртки:

fold :: Functor f => (f a -> a) -> (Fix f -> a)

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

данном случае рекурсивный тип будет начальным объектом. Функция развёртки строит из произвольного

типа данный рекурсивный тип, на языке теории категорий она строит стрелку из произвольного объекта в

рекурсивный, это означает что рекурсивный тип будет конечным объектом.

unfold :: Functor f => (a -> f a) -> (a -> Fix f)

Категории, которые определяют рекурсивные типы таким образом называются (ко)алгебрами функторов.

Видите в типе и той и другой функции стоит требование о том, что 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

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

⊥

F alse

Мы будем называть нетривиальными сравнения в которых, компоненты слева и справа от не равны. На-

пример ясно, что T rue

T rue или ⊥