функций высшего порядка на язык теории категорий, то мы получим стрелки, которые могут связывать дру-
гие стрелки. Категория с функциями высшего порядка может содержать свои стрелки в качестве объектов.
Стрелки как объекты обозначаются с помощью степени, так запись 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. Диаграмма говорит о том, что если мы каррированием
функции двух аргументов получим функцию высшего порядка C > BA, а затем с помощью функции eval
получим значение, то это всё равно, что подставить два значения в исходную функцию. Запись ( curry( f) , id)
означает параллельное применение двух стрелок внутри пары:
( f, g) : A ? A > B ? B ,
f : A > B, g : A > B
Так применив стрелки curry( f) : C > BA и id : A > A к паре C ? A, мы получим пару BA ? A.
Применение здесь условное мы подразумеваем применение в функциональной аналогии, в теории категорий
происходит связывание пар объектов с помощью стрелки ( f, g).
Интересно, что и экспоненту можно получить как конечный объект в специальной категории. Пусть есть
категория A и в ней определено произведение объектов A и B. Построим категорию, в которой объектами
являются стрелки вида:
C ? A > B
где C – это произвольный объект исходной категории. Стрелкой между объектами c : C ? A > B и
d : D ? A > B в этой категории будет стрелка f : C > D из исходной категории, такая, что следующая
диаграмма коммутирует:
C
C ? A
f
c
( f, id)
D
D ? A
B
Если в этой категории существует конечный объект, то он является экспонентой. А функция curry явля-
ется анаморфизмом для экспоненты.
238 | Глава 15: Теория категорий
15.9 Краткое содержание
Теория категорий изучает понятия через то как эти понятия взаимодействуют друг с другом. Мы забываем
о том, как эти понятия реализованы, а смотрим лишь на свойства связей.
Мы узнали что такое категория. Категория это структура с объектами и стрелками. Стрелки связывают
объекты. Причём связи могут соединятся. Также считается, что объект всегда связан сам с собой. Мы узнали,
что есть такие категории, в которых сами категории являются объектами, а стрелки в таких категориях мы
назвали функторами. Также мы узнали, что сами функторы могут стать объектами в некоторой категории,
тогда стрелки в этой категории мы будем называть естественными преобразованиями.
Мы узнали что такое начальный и конечный объект и как с помощью этих понятий можно определить
сумму и произведение типов. Также мы узнали как в теории категорий описываются функции высших по-
рядков.
15.10 Упражнения
• Проверьте аксиомы категории (ассоциативность и тождество) для категории функторов и категории
естественных преобразований.
• Изоморфизмом называют такие стрелки f : A > B и g : B > A, для которых выполнено свойство:
f ; g = idA
g ; f = idB
Объекты A и B называют изоморфными, если они связаны изоморфизмом, это обозначают так: A ?
= B.
Докажите, что все начальные и конечные элементы изоморфны.
• Поскольку сумма и произведение типов являются начальным и конечным объектами в специальных
категориях для них также выполняются свойства тождества, уникальности и слияния. Выпишите эти
свойства для суммы и произведения.
• Подумайте как можно определить экземпляр класса Comonad для потоков:
data Stream a = a :& Stream a
Можно ли придумать экземпляр для класса Monad?
• Дуальную категорию для категории A обозначают Aop. Если F является функтором в категории Aop,
то в исходной категории его называют контравариантным функтором. Выпишите определение функто-
ра в Aop, а затем с помощью дуализации получите свойства контравариантного функтора в исходной
категории A.
Краткое содержание | 239
Глава 16
Категориальные типы
В этой главе мы узнаем как в теории категорий определяются типы. В теории категорий типы определяют-
ся как начальные и конечные объекты в специальных категориях, которые называются алгебрами функторов.
Для понимания этой главы хорошо освежить в памяти главу о структурной рекурсии, там где мы говорили
о свёртках и развёртках.
16.1 Программирование в стиле оригами
Оригами – состоит из двух слов “свёртка” и “бумага”. При программировании в стиле оригами все функ-
ции строятся через функции свёртки и развёртки. Есть даже такие языки программрования, в которых это
единственный способ определения рекурсии. Этот стиль очень хорошо подходит для ленивых языков про-
граммирования, поскольку в связке:
fold f . unfold g
функции свёртки и развёртки работают синхронно. Функция развёртки не производит новых элементов
до тех пор пока они не понадобятся во внешней функции свёртки.
Помните в одной из глав мы говорили о том, что рекурсивные функции можно определять через функцию
fix.
Например так выглядит рекурсивная функция сложения всех чисел от одного до n:
sumInt :: Int -> Int
sumInt 0 = 0
sumInt n = n + sumInt (n—1)
Эту функцию мы можем переписать с помощью функции fix. При вычислении fix f будет составлено
значение
f (f (f (f … )))
Теперь перепишем функцию sumInt через fix:
sumInt = fix $ f n ->
case n of
0
-> 0
n
-> n + f (n — 1)
Смотрите лямбда функция в аргументе fix принимает функцию и число, а возвращает число. Тип этой
функции (Int -> Int) -> (Int -> Int). После применения функции fix мы как раз и получим функцию
типа Int -> Int. В лямбда функции рекурсивный вызов был заменён на вызов функции-параметра f.
Оказывается, что этот приём может быть применён и для рекурсивных типов данных. Мы можем создать
обобщённый тип, который обозначает рекурсивный тип:
newtype Fix f = Fix { unFix :: f (Fix f) }
В этой записи мы получаем уравнение неподвижной точки Fix f = f (Fix f), где f это некоторый тип
с параметром. Определим тип целых чисел:
240 | Глава 16: Категориальные типы
data N a = Zero | Succ a
type Nat = Fix N
Теперь создадим несколько конструкторов:
zero :: Nat
zero = Fix Zero
succ :: Nat -> Nat
succ = Fix . Succ
Сохраним эти определения в модуле Fix. hs и посмотрим в интерпретаторе на значения и их типы, ghc не
сможет вывести экземпляр Show для типа Fix, потому что он зависит от типа с параметром, а не от конкретно-
го типа. Для решения этой проблемы нам придётся определить экземпляры вручную и подключить несколько
расширений языка. Помните в главе о ленивых вычислениях мы подключали расширение BangPatterns? Нам
понадобятся:
{-# Language FlexibleContexts, UndecidableInstances #-}
Теперь определим экземпляры для Show и Eq:
instance Show (f (Fix f)) => Show (Fix f) where
