Законы Монады, выраженные в терминах объединения вместо привязки?
Традиции монады традиционно описываются в терминах >>= и pure:
pure a >>= k = k a
m >>= pure = m
m >>= (\x -> k x >>= h) = (m >>= k) >>= h
Однако, монады также могут быть определены в терминах join вместо >>=. Я хотел бы придумать формулировку законов монады в терминах join.
Используя x >>= f = join (fmap f x), его легко переписать существующие законы монады, чтобы устранить >>=. Упрощая результаты с помощью прикладных законов, первые два закона довольно приятно выражены:
join . pure = id
join . fmap pure = id
Интуиция для этих законов также проста, так как ясно, что введение дополнительного "слоя" с pure должно быть no-op в сочетании с join. Однако третий закон не так хорош. Он выглядит следующим образом:
join (fmap (\x -> join (fmap h (k x))) m)
= join (fmap h (join (fmap k m)))
Это не приятно уменьшает использование прикладных законов, и его гораздо труднее понять, не глядя на него какое-то время. У него, конечно же, нет такой же легкой интуиции.
Существует ли эквивалентная альтернативная формулировка законов монады в терминах join, которую легче понять? В качестве альтернативы, есть ли способ упростить вышеупомянутый закон или облегчить его поиск? Версия с >>= уже менее приятна, чем версия, выраженная композицией Kleisli, но версия с join почти нечитаема.
Ответы
Ответ 1
Украдены прямо из Википедии:
(Естественное преобразование η: 1 → T pure; естественное преобразование µ: T^2 → T является join)
µ. Tµ = µ. µT
В Хаскеле:
join . fmap join = join . join
По-английски: если вы начинаете с трех слоев монады как mmma :: Monad m => m (m (ma)), не имеет значения, будете ли вы сначала выравнивать его внутренний слой, а затем внешний, или сначала будете выравнивать его внешний слой и тогда внутренний. Это тот же закон, который вы указали в качестве третьего (ассоциативность).
µ. Tη = µ. ηT = 1
В Хаскеле:
join. fmap pure = join. pure = id
По-английски: если вы начинаете с одного слоя монады как ma :: Monad m => ma, не имеет значения, создаете ли вы новый слой внутри него, а затем выравниваете его, или если вы создаете новый слой вне него, а затем сгладить это, и оба - то же самое, что вообще ничего не делать. Этот закон является комбинацией ваших первых двух.
Кроме того, join является естественной трансформацией означает, что
join. fmap (fmap f) = fmap f. join
из-за параметричности.
