Unknown - haskell-notes

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

⊥ . Это тривиальные сравнения и мы их будем лишь подразумевать.

Считается, что если два значения определены полностью, то мы не можем сказать какое из них информатив-

нее. Так к примеру для логических значений мы не можем сказать какое значение более определено 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

Это требование накладывает запрет на возможность проведения сопоставления с образцом по значению