и получить категорию 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 или ?
?. Это тривиальные сравнения и мы их будем лишь подразумевать.
Считается, что если два значения определены полностью, то мы не можем сказать какое из них информатив-
нее. Так к примеру для логических значений мы не можем сказать какое значение более определено T rue
или F alse.
Рассмотрим пример по-сложнее. Частично определённые значения:
data M aybe a = N othing | Just a
Индуктивные и коиндуктивные типы | 245
?
N othing
?
J ust ?
?
J ust a
J ust a
J ust b,
если a
b
Если вспомнить как происходит вычисление значения, то значение a менее определено чем b, если взрыв-
ное значение ? в a находится ближе к корню значения, чем в b. Итак получается, что в категории Hask объ-
екты это множества с частичным порядком. Что означает требование монотонности функции?
Монотонность в контексте операции
говорит о том, что чем больше определён вход функции тем больше
определён выход:
a
b
? f a
f b
Это требование накладывает запрет на возможность проведения сопоставления с образцом по значению
?. Иначе мы можем определять немонотонные функции вроде:
isBot :: Bool -> Bool
isBot undefined = True
isBot _
= undefined
Полнота частично упорядоченного множества означает, что у любой последовательности xn
x 0
x 1
x 2
…
есть значение x, к которому она сходится. Это значение называют супремумом множества. Что такое
полные частично упорядоченные множества мы разобрались. А что такое полиномиальный функтор?
Полиномиальный функтор
Полиномиальный функтор – это функтор который построен лишь с помощью операций суммы, произве-
дения, постоянных функторов, тождественного фуктора и композиции функторов. Определим эти операции:
• Сумма функторов F и G определяется через операцию суммы объектов:
( F + G) X = F X + GX
• Произведение функторов F и G определяется через операцию произведения объектов:
( F ? G) X = F X ? GX
• Постоянный функтор отображает все объекты категории в один объект, а стрелки в тождественнубю
стрелку этого объекта, мы будем обозначать постоянный функтор подчёркиванием:
AX
=
A
Af
=
idA
• Тождественный функтор оставляет объекты и стрелки неизменными:
IX
=
X
If
=
f
• Композиция функторов F и G это последовательное применение функторов
F GX = F ( GX)
246 | Глава 16: Категориальные типы
По определению функции построенные с помощью этих операций называют полиномиальными. Опреде-
лим несколько типов данных с помощью полиномиальных функторов. Определим логические значения:
Bool = µ(1 + 1)
Объект 1 обозначает любую константу, это конечный объект исходной категории. Нам не важны имена
конструкторов, но важна структура типа. µ обозначает начальный объект в F -алгебре.
Определим натуральные числа:
N at = µ(1 + I)
Эта запись обозначает начальный объект для F -алгебры с функтором F = 1 + I. Посмотрим на опреде-
ление списка:
ListA = µ(1 + A ? I)
Список это начальный объект F -алгебры 1 + A ? I. Также можно определить бинарные деревья: