Unknown - haskell-notes

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

кают голову и хвост списка:

headL :: Lista ->a

headL x = caseunFix x of

Nil

-> error”empty list”

Consa _

->a

tailL :: Lista -> Lista

tailL x = caseunFix x of

Nil

-> error”empty list”

Consa b

->b

Теперь определим несколько новых функций:

mapL ::(a ->b) -> Lista -> Listb

mapL f =fold $\x -> casex of

Nil

->nil

Consa b

->f a ‘cons‘ b

takeL :: Int -> Lista -> Lista

takeL =curry $unfold $\(n, xs) ->

ifn ==0 then Nil

else Cons(headL xs) (n -1, tailL xs)

Сравните эти функции с теми, что мы определяли в главе о структурной рекурсии. Проверим работают

ли эти функции:

*Fix> :r

[1 of1] 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> letx =1 ‘cons‘ 2 ‘cons‘ 3 ‘cons‘ nil

*Fix>mapL ( +10) $x ‘concatL‘ x

( Cons11 ( Cons12 ( Cons13 ( Cons11 ( Cons12 ( Cons13 ( Nil)))))))

Обратите внимание, на то что с большими буквами мы пишем Consи Nilкогда хотим закодировать

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

разобрались на примерах как устроены функции fold и unfold, потому что теперь мы перейдём к теории,

которая за этим стоит.

Программирование в стиле оригами | 243

16.2 Индуктивные и коиндуктивные типы

С точки зрения теории категорий функция свёртки является катаморфизмом, а функция развёртки – ана-

морфизмом. Напомню, что катаморфизм – это функция которая ставит в соответствие объектам категории

с начальным объектом стрелки, которые начинаются из начального объекта, а заканчиваются в данном объ-

екте. Анаморфизм – это перевёрнутый наизнанку катаморфизм.

Начальным и конечным объектом будет рекурсивный тип. Вспомним тип свёртки:

fold :: Functorf =>(f a ->a) ->( Fixf ->a)

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

данном случае рекурсивный тип будет начальным объектом. Функция развёртки строит из произвольного

типа данный рекурсивный тип, на языке теории категорий она строит стрелку из произвольного объекта в

рекурсивный, это означает что рекурсивный тип будет конечным объектом.

unfold :: Functorf =>(a ->f a) ->(a -> Fixf)

Категории, которые определяют рекурсивные типы таким образом называются (ко)алгебрами функторов.

Видите в типе и той и другой функции стоит требование о том, что 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 , для которой выполняется: