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
Но в лямбда-исчислении нам были доступны более гибкие функции, функции могли принимать на вход
функции и возвращать функции. Как с этим обстоят дела в теории категорий? Если перевести определение
функций высшего порядка на язык теории категорий, то мы получим стрелки, которые могут связывать дру-
гие стрелки. Категория с функциями высшего порядка может содержать свои стрелки в качестве объектов.
Стрелки как объекты обозначаются с помощью степени, так запись BA означает стрелку A → B. При этом
нам необходимо уметь интерпретировать стрелку, мы хотим уметь подставлять значения. Если у нас есть
объект BA, то должна быть стрелка
eval : BA × A → B
На языке функций можно сказать, что стрелка eval принимает функцию высшего порядка A → B и зна-
чение типа A, а возвращает значение типа B. Объект BA называют экспонентой. Теперь дадим формальное
определение.
Пусть в категории A определено произведение. Экспонента – это объект BA вместе со стрелкой eval :
BA × A → B такой, что для любой стрелки f : C × A → B определена стрелка curry( f ) : C → BA при
этом следующая диаграмма коммутирует:
C