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

Question

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

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

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

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

2. Распакованный вывод m передается в returnэто переворачивает это.Монадная природа остается прежней.Таким образом, это то же самое, что и исходная монада.

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

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

Answer 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) Ассоциативность - монадная композиция ассоциативна (мне нравится ответ Кенни ТМ за это)

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

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

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

Answer 2

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

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

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

1. id . f эквивалентно f
2. f . id эквивалентно f
3. (f . g) . h эквивалентно f . (g . h)

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

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

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

1. [] ++ xs эквивалентно xs
2. xs ++ [] эквивалентно xs
3. (xs ++ ys) ++ zs эквивалентно xs ++ (ys ++ zs)

---

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

Answer 3

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

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

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

Answer 4

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

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

do
   x <- foo
   bar x
   z <- baz

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

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

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

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