instance Num Nat where
(+) a = fold $ x -> case x of
Zero
-> a
Succ x
-> succ x
(*) a = fold $ x -> case x of
242 | Глава 16: Категориальные типы
Zero
-> zero
Succ x
-> a + x
fromInteger = unfold $ n -> case n of
0
-> Zero
n
-> Succ (n—1)
abs = undefined
signum = undefined
Сложение и умножение определены через свёртку, а функция построения натурального числа из чис-
ла типа Integer определена через развёртку. Сравните с теми функциями, которые мы писали в главе про
структурную рекурсию. Теперь мы не передаём отдельно две функции, на которые мы будем заменять кон-
структоры. Эти функции закодированы в типе с параметром. Для того чтобы этот код заработал нам придётся
добавить ещё одно расширение TypeSynonymInstances наши рекурсивные типы являются синонимами, а не
новыми типами. В рамках стандарта Haskell мы можем определять экземпляры только для новых типов, для
того чтобы обойти это ограничение мы добавим ещё одно расширение.
*Fix> succ $ 1+2
(Succ (Succ (Succ (Succ (Zero)))))
*Fix> ((2 * 3) + 1) :: Nat
(Succ (Succ (Succ (Succ (Succ (Succ (Succ (Zero))))))))
*Fix> 2+2 == 2*(2::Nat)
True
Определим функции на списках. Для начала определим две вспомогательные функции, которые извле-
кают голову и хвост списка:
headL :: List a -> a
headL x = case unFix x of
Nil
-> error ”empty list”
Cons a _
-> a
tailL :: List a -> List a
tailL x = case unFix x of
Nil
-> error ”empty list”
Cons a b
-> b
Теперь определим несколько новых функций:
mapL :: (a -> b) -> List a -> List b
mapL f = fold $ x -> case x of
Nil
-> nil
Cons a b
-> f a ‘cons‘ b
takeL :: Int -> List a -> List a
takeL = curry $ unfold $ (n, xs) ->
if n == 0 then Nil
else Cons (headL xs) (n—1, tailL xs)
Сравните эти функции с теми, что мы определяли в главе о структурной рекурсии. Проверим работают
ли эти функции:
*Fix> :r
[1 of 1] Compiling Fix
( Fix. hs, interpreted )
Ok, modules loaded: Fix.
*Fix> takeL 3 $ iterateL (+1) zero
(Cons (Zero) (Cons (Succ (Zero)) (Cons (Succ (Succ (Zero))) (Nil))))
*Fix> let x = 1 ‘cons‘ 2 ‘cons‘ 3 ‘cons‘ nil
*Fix> mapL (+10) $ x ‘concatL‘ x
(Cons 11 (Cons 12 (Cons 13 (Cons 11 (Cons 12 (Cons 13 (Nil)))))))
Обратите внимание, на то что с большими буквами мы пишем Cons и Nil когда хотим закодировать
функции для свёртки-развёртки, а с маленькой буквы пишем значения рекурсивного типа. Надеюсь, что вы
разобрались на примерах как устроены функции fold и unfold, потому что теперь мы перейдём к теории,
которая за этим стоит.
Программирование в стиле оригами | 243
16.2 Индуктивные и коиндуктивные типы
С точки зрения теории категорий функция свёртки является катаморфизмом, а функция развёртки – ана-
морфизмом. Напомню, что катаморфизм – это функция которая ставит в соответствие объектам категории
с начальным объектом стрелки, которые начинаются из начального объекта, а заканчиваются в данном объ-
екте. Анаморфизм – это перевёрнутый наизнанку катаморфизм.
Начальным и конечным объектом будет рекурсивный тип. Вспомним тип свёртки:
fold :: Functor f => (f a -> a) -> (Fix f -> a)
Функция свёртки строит функции, которые ведут из рекурсивного типа в произвольный тип, поэтому в
данном случае рекурсивный тип будет начальным объектом. Функция развёртки строит из произвольного
типа данный рекурсивный тип, на языке теории категорий она строит стрелку из произвольного объекта в
рекурсивный, это означает что рекурсивный тип будет конечным объектом.
unfold :: Functor f => (a -> f a) -> (a -> Fix f)
Категории, которые определяют рекурсивные типы таким образом называются (ко)алгебрами функторов.
Видите в типе и той и другой функции стоит требование о том, что f является функтором. Катаморфизм и
анаморфизм отображают объекты в стрелки. По типу функций fold и unfold мы можем сделать вывод, что
объектами в нашей категории будут стрелки вида
f a -> a
или для свёрток:
a -> f a
А стрелками будут обычные функции одного аргумента. Теперь дадим более формальное определение.
Эндофунктор F : A > A определяет стрелки ? : F A > A, которые называется F — алгебрами. Стрелку
h : A > B называют F — гомоморфизмом, если следующая диаграмма коммутирует:
F A
?
A
F h
h
F B
B
?
Или можно сказать по другому, для F -алгебр ? : F A > A и ? : F B > B выполняется:
F h ; ? = ? ; h
Это свойство совпадает со свойством естественного преобразования только вместо одного из функторов
мы подставили тождественный функтор I. Определим категорию Alg( F ), для категории A и эндофунктора
F : A > A
• Объектами являются F -алгебры F A > A, где A – объект категории A
• Два объекта ? : F A > A и ? : F B > B соединяет F -гомоморфизм h : A > B. Это такая стрелка из
A, для которой выполняется:
F h ; ? = ? ; h
• Композиция и тождественная стрелка взяты из категории A.
Если в этой категории есть начальный объект inF : F T > T , то определён катаморфизм, который
переводит объекты F A > A в стрелки T > A. Причём следующая диаграмма коммутирует:
in
F T
F
T
F ( | ? |)
( | ? |)
F A
A
?
Этот катаморфизм и будет функцией свёртки для рекурсивного типа . Понятие Alg( F ) можно перевернуть