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 ⊥
⊥