52700.fb2
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.
Оказывается, что этот приём может быть применён и для рекурсивных типов данных. Мы можем создать