Объяснение законов Монады

Из нежное введение в Haskell, есть следующие законы монады. Может ли кто-нибудь интуитивно объяснить, что они означают?

return a >>= k             = k a
m >>= return               = m
xs >>= return . f          = fmap f xs
m >>= (\x -> k x >>= h)    = (m >>= k) >>= h

Вот мое объяснение:

  • Мы ожидаем, что возвращаемая функция обернется a, чтобы ее монадическая природа была тривиальной. Когда мы привязываем его к функции, нет никаких монадических эффектов, она должна просто передать a функции.

  • Развернутый вывод m передается для возврата, который переустанавливает его. Монадическая природа остается прежней. Так что это то же самое, что и оригинальная монада.

  • Развернутое значение передается в f, затем перезаписывается. Монадическая природа остается прежней. Это поведение, ожидаемое при преобразовании нормальной функции в монадическую функцию.

  • У меня нет объяснения этого закона. Это говорит о том, что монада должна быть "почти ассоциативной", хотя

Ответы

Ответ 1

Ваши описания выглядят неплохо. Как правило, люди говорят о трех монадских законах, которые у вас есть как 1, 2 и 4. Ваш третий закон несколько отличается, и я позабочусь об этом позже.

Для трех законов монады мне гораздо легче получить интуитивное понимание того, что они означают, когда они переписаны с использованием композиции Клейсли:

-- defined in Control.Monad
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
mf >=> n = \x -> mf x >>= n

Теперь законы могут быть записаны как:

1) return >=> mf = mf                  -- left identity
2) mf >=> return = mf                  -- right identity
4) (f >=> g) >=> h = f >=> (g >=> h)   -- associativity

1) Закон левой идентичности - возврат значения не изменяет значение и ничего не делает в монаде.

2) Право прав личности - возврат значения не изменяет значение и ничего не делает в монаде.

4) Ассоциативность - монадическая композиция ассоциативна (мне нравится ответ KennyTM для этого)

Два закона идентичности в основном говорят одно и то же, но они оба необходимы, потому что return должно иметь поведение идентичности с обеих сторон оператора привязки.

Теперь для третьего закона. Этот закон по сути говорит, что и экземпляр Functor, и ваш экземпляр Monad ведут себя одинаково, когда поднимают функцию в монаду, и что она не делает ничего монадического. Если я не ошибаюсь, то случай, когда монада подчиняется другим трем законам, и экземпляр Functor подчиняется законам функтора, тогда это утверждение всегда будет истинным.

Многое из этого происходит из Haskell Wiki. Typeclassopedia также является хорошей ссылкой.

Ответ 2

Никаких разногласий с другими ответами, но это могло бы помочь думать о законах монады, как фактически описывая два набора свойств. Как говорит Джон, третий закон, который вы упоминаете, немного отличается, но здесь, как другие могут быть разделены:

Функции, которые вы связываете с монадой, составлены так же, как обычные функции.

Как и в ответе Джона, так называемая стрелка Клейсли для монады - это функция с типом a -> m b. Подумайте о return как id и (<=<) как (.), а законы монады - их переводы:

  • id . f эквивалентен f
  • f . id эквивалентен f
  • (f . g) . h эквивалентен f . (g . h)

Последовательности монадических эффектов добавляются как списки.

По большей части вы можете думать о дополнительной монадической структуре как о последовательности дополнительных действий, связанных с монадическим значением; например Maybe "сдаваться" для Nothing и "продолжать движение" для Just. Объединение двух монадических действий затем по существу объединяет последовательности поведения, которые они проводили.

В этом смысле return снова является тождеством - нулевое действие, похожее на пустой список поведения, и (>=>) является конкатенацией. Итак, монадские законы являются их переводами:

  • [] ++ xs эквивалентно xs
  • xs ++ [] эквивалентен xs
  • (xs ++ ys) ++ zs эквивалентен xs ++ (ys ++ zs)

Эти три закона описывают смехотворно общую картину, которую Хаскелл, к сожалению, не может выразить в полной общности. Если вам интересно, Control.Category дает обобщение "вещей, которые выглядят как состав функций", а Data.Monoid обобщает последний случай, когда не задействованы никакие параметры типа.

Ответ 3

В терминах обозначения do правило 4 означает, что мы можем добавить дополнительный блок do для группировки последовательности монадических операций.

    do                          do
                                  y <- do
      x <- m                             x <- m
      y <- k x          <=>              k x
      h y                         h y

Это позволяет функциям, которые возвращают монадическое значение, работает правильно.

Ответ 4

Первые три закона говорят, что "возврат" только обертывает значение и ничего не делает. Таким образом, вы можете исключить "возвратные" вызовы без изменения семантики.

Последний закон - ассоциативность связывания. Это означает, что вы берете что-то вроде:

do
   x <- foo
   bar x
   z <- baz

и превратите его в

do
   do
      x <- foo
      bar x
   z <- baz

без изменения значения. Конечно, вы не сделали бы этого, но вы можете поместить внутреннее предложение do в оператор "if" и хотите, чтобы это означало то же самое, когда "if" истинно.

Иногда монады точно не следуют этим законам, особенно когда происходит какое-то нижнее значение. Это нормально, пока оно задокументировано и является "морально правильным" (т.е. Законы соблюдаются для не-нижних значений или результаты считаются эквивалентными каким-либо другим способом).