Выбрать главу

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. Также можно определить бинарные деревья:

BT reeA = µ( A + I × I)

Определим потоки:

StreamA = ν( A × I)

Потоки являются конечным объектом F -коалгебры, где F = A × I.

16.3 Гиломорфизм

Оказывается, что с помощью катаморфизма и анаморфизма мы можем определить функцию fix, то есть

мы можем выразить любую рекурсивную функцию с помощью структурной рекурсии.