представляют собой сумму и произведение в общем случае. Тип для суммы это Either:
data Either a b = Left a | Right b
Произведение в самом общем виде представлено кортежами:
data (a, b) = (a, b)
В теории категорий сумма и произведение определяются как начальный и конечный объекты в специаль-
ных категориях. Теория категорий изучает объекты по тому как они взаимодействуют с остальными объек-
тами. Взаимодействие обозначается с помощью стрелок. Специальные свойства стрелок определяют объект.
Например представим, что мы не можем заглядывать внутрь суммы типов, как бы мы могли взаимодей-
ствовать с объектом, который представляет собой сумму двух типов A+ B? Нам необходимо уметь создавать
объект типа A + B из объектов A и B извлекать их из суммы. Создание объектов происходит с помощью
двух специальных конструкторов:
inl : A > A + B
inr : B > A + B
Сумма и произведение | 235
Также нам хочется уметь как-то извлекать значения. По смыслу внутри суммы A+ B хранится либо объект
A либо объект B и мы не можем заранее знать какой из них, поскольку внутреннее содержание A + B от
нас скрыто, но мы знаем, что это только A или B. Это говорит о том, что если у нас есть две стрелки A > C
и B > C, то мы как-то можем построить A + B > C. У нас есть операция:
out( f, g) : A + B > C
f : A > C, g : B > C
При этом для того, чтобы стрелки inl, inr и out были согласованы необходимо, чтобы выполнялись
свойства:
inl ; out( f, g) = f
inr ; out( f, g) = g
Для любых функций f и g. Графически это свойство можно изобразить так:
A
inl
A + B
inr
B
out
f
g
C
Итак суммой двух объектов A и B называется объект A + B и две стрелки inl : A > A + B и inr : B >
A + B такие, что для любых двух стрелок f : A > C и g : B > C определена одна и только одна стрелка
h : A + B > C такая, что выполнены свойства:
inl ; h = f
inr ; h = g
В этом определении объект A + B вместе со стрелками inl и inr, определяет функцию, которая по
некоторому объекту C и двум стрелкам f и g строит стрелку h, которая ведёт из объекта A + B в объект
C. Этот процесс определения стрелки по объекту напоминает определение начального элемента. Построим
специальную категорию, в которой объект A+ B будет начальным. Тогда функция out будет катаморфизмом.
Функция out принимает две стрелки и возвращает третью. Посмотрим на типы:
f : A > C
inl : A > A + B
g : B > C
inr : B > A + B
Каждая из пар стрелок в столбцах указывают на один и тот же объект, а начинаются они из двух разных
объектов A и B. Определим категорию, в которой объектами являются пары стрелок ( a 1 , a 2), которые на-
чинаются из объектов A и B и заканчиваются в некотором общем объекте D. Эту категорию ещё называют
клином. Стрелками в этой категории будут такие стрелки f : ( d 1 , d 2) > ( e 1 , e 2), что стрелки в следующей
диаграмме коммутируют (не важно по какому пути идти из двух разных точек).
A
B
d
e
1
2
e 1
d 2
D
E
f
Композиция стрелок – это обычная композиция в исходной категории, в которой определены объекты A
и B, а тождественная стрелка для каждого объекта, это тождественная стрелка для того объекта, в котором
сходятся обе стрелки. Можно проверить, что это действительно категория.
Если в этой категории есть начальный объект, то мы будем называть его суммой объектов A и B. Две
стрелки, которые содержит этот объект мы будем называть inl и inr, а общий объект в котором эти стрелки
сходятся будем называть A + B. Теперь если мы выпишем определение для начального объекта, но вме-
сто произвольных стрелок и объектов подставим наш конкретный случай, то мы получим как раз исходное
определение суммы.
Начальный объект ( inl : A > A + B, inr : B > A + B) ставит в соответствие любому объекту
( f : A > C, g : B > C) стрелку h : A + B > C такую, что выполняются свойства:
236 | Глава 15: Теория категорий
A
inl
A + B
inr
B
h
f
g
C
А как на счёт произведения? Оказывается, что произведение является дуальным понятием по отношению
к сумме. Его иногда называют косуммой, или сумму называют копроизведением. Дуализируем категорию,
которую мы строили для суммы.
У нас есть категория A и в ней выделено два объекта A и B. Объектами новой категории будут пары
стрелок ( a 1 , a 2), которые начинаются в общем объекте C а заканчиваются в объектах A и B. Стрелками в
этой категории будут стрелки исходной категории h : ( e 1 , e 2) > ( d 1 , d 2) такие что следующая диаграмма
коммутирует:
A
B
e 1
d 2
d
e
1
2
D
E
f
Композиция и тождественные стрелки позаимствованы из исходной категории A. Если в этой категории
существует конечный объект. То мы будем называть его произведением объектов A и B. Две стрелки этого
объекта обозначаются как ( exl, exr), а общий объект из которого они начинаются мы назовём A?B. Теперь
распишем определение конечного объекта для нашей категории пар стрелок с общим началом.
Конечный объект ( exl : A?B > A, exr : A?B > B) ставит в соответствие любому объекту категории
( f : C > A, g : C > B) стрелку h : C > A ? B. При этом выполняются свойства:
A
exl
A ? B
exr
B
h
f
g
C
Итак мы определили сумму, а затем на автомате, перевернув все утверждения, получили определение
произведения. Но что это такое? Соответствует ли оно интуитивному понятию произведения?
Так же как и в случае суммы в теории категорий мы определяем понятие, через то как мы можем с ним
взаимодействовать. Посмотрим, что нам досталось от абстрактного определения. У нас есть обозначение
произведения типов A ? B. Две стрелки exl и exr. Также у нас есть способ получить по двум функциям
f : C > A и g : C > B стрелку h : C > A ? B. Для начала посмотрим на типы стрелок конечного объекта:
exl : A ? B > A
exr : A ? B > B
По типам видно, что эти стрелки разбивают пару на составляющие. По смыслу произведения мы точно
знаем, что у нас есть в A ? B и объект A и объект B. Эти стрелки позволяют нам извлекать компоненты
пары. Теперь посмотрим на анаморфизм:
[( f, g )] : C > A ? B
f : C > A, g : C > B
Эта функция позволяет строить пару по двум функциям и начальному значению. Но, поскольку здесь мы
ничего не вычисляем, а лишь связываем объекты, мы можем по паре стрелок, которые начинаются из общего
источника связать источник с парой конечных точек A ? B.
При этом выполняются свойства:
[( f, g )] ; exl = f
[( f, g )] ; exr = g
Эти свойства говорят о том, что функции построения пары и извлечения элементов из пары согласованы.
Если мы положим значение в первый элемент пары и тут же извлечём его, то это тоже само если бы мы не
использовали пару совсем. То же самое и со вторым элементом.
Сумма и произведение | 237
15.8 Экспонента
Если представить, что стрелки это функции, то может показаться, что все наши функции являются функ-
циями одного аргумента. Ведь у стрелки есть только один источник. Как быть если мы хотим определить
функцию нескольких аргументов, что она связывает? Если в нашей категории определено произведение объ-
ектов, то мы можем представить функцию двух аргументов, как стрелку, которая начинается из произведе-
ния:
(+) : N um ? N um > N um
Но в лямбда-исчислении нам были доступны более гибкие функции, функции могли принимать на вход
функции и возвращать функции. Как с этим обстоят дела в теории категорий? Если перевести определение
