?

Log in

No account? Create an account
Previous Entry Share Next Entry
Kleisli + List
eye
voidex
Возьмём Клейсли-категорию для монады Writer. Затем определим функтор такой, что
F(a) = 1 + a * F(a) -- список
F(f) = id + f * F(f)
  -- null -> null
  -- (x, xs) -> (f x, F(f) xs)

где + и * в F(f)choose и parcomp

Но в таком случае, если я ничего не путаю, не соблюдается F(f . g) = F(f) . F(g)

Действительно, возьмём f, пишущий "f" и возвращающий свой аргумент, и g — пишущий "g".
Тогда f . g допишет "fg".
F(f) [1,1,1] — "fff"
F(g) [1,1,1] — "ggg"
F(f . g) [1,1,1] — "fgfgfg"
F(f) . F(g) [1,1,1] — "fffggg"


Кто виноват и что делать?

  • 1
Определись - F - это функтор чего? Списка или Writer?

Если Writer, то F(f) [1,1,1] напишет один "f"
Если списка, то F(f).F(g) вернёт writer-ы, которые пишут "fg"

"fffggg" не будет ни в одном из случаев.

F - списочный эндофунктор на Клейсли-категории для Writer.

Каждому a из Клейсли-категории ставит в соответствие [a]
Каждому морфизму a -w-> b ставит в соответствие [a] -w-> [b]
где a -w-> b — морфизм в Клейсли-категории.

Т.е. переводя на Hask:
map : (a -> Writer String b) -> [a] -> Writer String [b]
И вот как написать этот map, чтобы map f . map g === map (f . g)?

> Каждому морфизму a -w-> b ставит в соответствие [a] -w-> [b]

Что-то непонятно, у этой категории кодомен должен быть Writer a.

Насчёт Hask - какие типы у f и g?

Я не спец в этих технологиях, поэтому расскажу на пальцах, как я это понимаю. Если неправильно понимаю, поправьте меня.

Возьмем категорию K. Объекты — типы, морфизмы — K a b = a -> Writer b, (.) = (>=>)
Теперь возьмём такой "эндофунктор" F : K -> K:
F(a) = [a]
для каждого f : K a b имеем F(f) : K [a] [b]
K [a] [b] = [a] -> Writer [b]

В общем-то, это не функтор, так как у него не соблюдается F(f) . F(g) = F(f . g)

Если до этого момента я не допустил ошибок в рассуждениях, то продолжаем дальше

Списочный map (обычный, функтор Set -> Set) можно определить в терминах стрелок (тоже обычных) как:
1. list(A) = 1 + A * list(A)
2. map f = id + f * map f

Теперь возьмём стрелки Клейсли (в нашем примере K) и попробуем записать то же:
mapK (f : K a b) = id + f * mapK f
mapK : K a b -> K [a] [b]

Получили mapM для монады Writer, однако это уже не функтор. Причём порядок "обхода" списка (mapM = sequence . map) заложен в определении стрелки клейсли, там явно описано, что произведение функций сначала обрабатывает первый элемент, а потом уже второй, соединяя это всё монадическим bind.
Хотя по факту мы могли бы определить другую стрелку Клейсли, получив обратный обход списка.

И наконец последняя мысля.

Если дан map для списочного эндофунктора над Set
То мы можем получить монадические mapM
1. обход вперёд: sequence . map
2. обход назад: rsequence . map (где rsequence очевиден)
При этом sequence и rsequence по сути коммутаторы для [Writer a] -> Writer [a], но нарушающие закон функтора.

Если же дана генерализованная функция mapK = id + f * mapK f, то
1. Обычная получается переносом на обычные стрелки
2. Монадическая с обходом вперёд - Клейсли
3. Монадическая с обходом назад - Клейсли с другим определением для умножения стрелок (сначала второй элемент, затем первый)

Я вижу в этом какую-то общность, одно выражается через другое, но я не знаю, нет ли какой-то абстракции для всего этого?

Т.е. иметь две функции map и mapM кажется странным, они одинаковые. С другой стороны вторая - не функтор, поэтому не получится нарисовать какой-то обобщённый функтор с этой генерализованной mapK.
Т.е. она должна быть написана отдельно. Тогда map для эндофунктора Set -> Set будет всего лишь mapK для обычных стрелок, а mapM будет mapK для соответствующих монадических стрелок. Но что такое mapK?

Хм, а откуда следует, что эндофунктор, определённый на основной категории, расширяется на категорию Клейсли?
F(a → Tb) |→ F(a) → T(F(b)) - не видно, почему бы так. Ну хотя бы коммутировать должен с Т.

Так и не следует.

Просто map и mapM в терминах стрелок выглядят одинаково, что наталкивает на некую общность, но при этом первая — функтор, а вторая — нет. Ну да и чёрт бы с ней, но есть ли какая-то абстракция для mapM? Она почти как функтор, но вот закон не соблюдается.

Если я правильно понимаю, то морфизмы категории Клейсли для такого функтора будут устроены так: a -w-> [b], то есть a -> Writer log [b] - что то же самое, что морфизмы категории Клейсли для монады ListT (Writer log).

То есть, то, что ты говоришь, означает, по сути, что монадический трансформер ListT - неправильный. Это - давно известный факт, и на Haskell wiki есть способы исправить его: http://www.haskell.org/haskellwiki/ListT_done_right для начала.

Не очень понимаю.
Если есть функтор F : S -> T, то для каждого морфизма f : S a b ставится в соответствие F(f) : T F(a) F(b)
В данном случае я беру категорию K (Kleisli для Writer), где объекты - типы, а морфизмы K a b = a -> Writer b

Затем я беру F : K -> K такой, что для каждого типа a
F(a) = List(a)
А для каждого морфизма f : K a b
F(f) есть морфизм K F(a) F(b), т.е. K List(a) List(b)
Т.е. List(a) -> Writer (List(b))

Далее, если я правильно понимаю, имея соответствующее натуральное преобрвазование Writer . List -> List . Writer
Мы сможем таки получить одновременно и описанную тобой монаду, и функтор, который хочу я, так?

В общем, я склоняюсь к мысли, что это слабо нужно, так как даже со списком мы можем обходить в одну сторону (как mapM), так и в обратную, и в обоих случаях это нарушит "функторность", но тем не менее сама по себе mapM кажется достаточно практичной функцией.
На деревьях уже сложнее, там (в случае Branch a (Tree a) (Tree a) например) вариантов обхода уже 3 и ни на какие стрелки это не ляжет (так как в стрелке Клейсли можно задать только два варианта: прямой порядок для тупла или обратный)
Поэтому логичным кажется всё же иметь обычный эндофунктор на Set (т.е. простой map), а нужный порядок организовывать соответствующей функцией (в случае mapM - sequence).

Ссылку почитаю, спасибо.

  • 1