Что является примером неправильной монады, которая нарушает закон ассоциативности?

Question

Фоновый контекст:

Математически я вижу потребность в ассоциативности для упрощения без учета порядка. Все реализации примеров монад, с которыми я сталкивался (блоги, книги и т. Д. 1055 *.,), Кажется, всегда работают . Кажется, просто акт наличия map, flatMap (Scala) или fmap, >>= (Haskell) делает вещи работающей монадой.

Из того, что я понял, это не совсем верно, но может ' Придумайте встречный пример, показывающий «необходимость» закона в случае неудачи.

В работе Вадлера упоминается возможность неправильной реализации:

Haskell Вики упоминает следующее:

Третий закон является своего рода законом ассоциативности для >>=. Подчинение трем l aws гарантирует, что семантика do-нотации, использующей монаду, будет согласованной.

Любой конструктор типов с операторами return и bind, которые удовлетворяют трем монадам l aws, является монадой. В Haskell компилятор не проверяет, сохраняется ли l aws для каждого экземпляра класса Monad. Программист должен убедиться, что любой созданный им экземпляр Монады удовлетворяет монаде l aws.

Вопрос (ы):

1. Что является примером неправильной реализации монады, когда выглядит правильно , но нарушает ассоциативность?
2. Как это влияет на do -обозначение?
3. Как это сделать проверить правильность реализации монады? Нужно ли писать тестовые случаи для каждой новой монады, или можно написать обобщенный c, чтобы проверить правильность реализации любой монады?

Answer 1

Вот пример немонады, которая не справляется с ассоциативностью:

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad

newtype ListIO a = L { runListIO :: IO [a] }
  deriving Functor

instance Applicative ListIO where
   pure x = L $ return [x]
   (<*>) = ap

instance Monad ListIO where
   (L m) >>= f = L $ do
      xs <- m
      concat <$> mapM (runListIO . f) xs

Если ассоциативность удовлетворена, эти два do блока будут эквивалентны

act1 :: ListIO Int
act1 = do
   L (pure [1,2,3])
   do L (putStr "a" >> return [10])
      L (putStr "b" >> return [7])

act2 :: ListIO Int
act2 = do
   do L (pure [1,2,3])
      L (putStr "a" >> return [10])
   L (putStr "b" >> return [7])

Однако, запуск Действия выдают разные результаты:

main :: IO ()
main = do
   runListIO act1 -- ababab
   putStrLn ""
   runListIO act2 -- aaabbb
   return ()

В общем случае утверждение закона ассоциативности может быть трудным. Конечно, можно написать тесты, но идеальным способом обеспечения ассоциативности было бы написать математическое доказательство закона. В некоторых случаях для доказательства ассоциативности достаточно эквационального мышления. Иногда нам также нужна индукция.