Unknown - haskell-notes

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

Но в лямбда-исчислении нам были доступны более гибкие функции, функции могли принимать на вход

функции и возвращать функции. Как с этим обстоят дела в теории категорий? Если перевести определение

функций высшего порядка на язык теории категорий, то мы получим стрелки, которые могут связывать дру-

гие стрелки. Категория с функциями высшего порядка может содержать свои стрелки в качестве объектов.

Стрелки как объекты обозначаются с помощью степени, так запись 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

C × A

f

curry ( f )

( curry ( f ) , id )

BA

BA × A

B

Давайте разберёмся, что это всё означает. По смыслу стрелка curry ( f ) это каррированная функция двух

аргументов. Вспомните о функции curry из Haskell. Диаграмма говорит о том, что если мы каррированием