Конкретный пример, показывающий, что монады не закрыты по составу (с доказательством)?


ответ дает [String -> a] в качестве примера не-монады. Поиграв с ним немного, я верю в это интуитивно, но этот ответ просто говорит: "соединение не может быть реализовано", не давая никакого оправдания. Я бы хотел кое-что более формальный. Конечно, есть много функций типа [String -> [String -> a]] -> [String -> a]; нужно показать, что любая такая функция обязательно не удовлетворяет законам монады.

любой пример (с сопровождающим доказательством) будет делать; я не обязательно ищу доказательство приведенного выше примера в частности.

4 75

4 ответа:

рассмотрим эту монаду, которая изоморфна (Bool ->) монады:

data Pair a = P a a

instance Functor Pair where
  fmap f (P x y) = P (f x) (f y)

instance Monad Pair where
  return x = P x x
  P a b >>= f = P x y
    where P x _ = f a
          P _ y = f b

и составьте его с Maybe монады:

newtype Bad a = B (Maybe (Pair a))

я утверждаю, что Bad не может быть монадой.


частичное доказательство:

есть только один способ определить fmap, что соответствует fmap id = id:

instance Functor Bad where
    fmap f (B x) = B $ fmap (fmap f) x

вспомните законы монады:

(1) join (return x) = x 
(2) join (fmap return x) = x
(3) join (join x) = join (fmap join x)

для определения return x, у нас есть два варианта: B Nothing или B (Just (P x x)). Понятно, что для того, чтобы иметь хоть какую-то надежду на возвращение x из (1) и (2), мы не можем выбросить x, поэтому мы должны выбрать второй вариант.

return' :: a -> Bad a
return' x = B (Just (P x x))

оставляет join. Поскольку есть только несколько возможных входов, мы можем сделать случай для каждого:

join :: Bad (Bad a) -> Bad a
(A) join (B Nothing) = ???
(B) join (B (Just (P (B Nothing)          (B Nothing))))          = ???
(C) join (B (Just (P (B (Just (P x1 x2))) (B Nothing))))          = ???
(D) join (B (Just (P (B Nothing)          (B (Just (P x1 x2)))))) = ???
(E) join (B (Just (P (B (Just (P x1 x2))) (B (Just (P x3 x4)))))) = ???

так как выход имеет тип Bad a, только варианты B Nothing или B (Just (P y1 y2)) здесь y1,y2 должны быть выбраны из x1 ... x4.

In случаи (А) и (б), у нас нет значений типа a, так что мы вынуждены вернуться B Nothing в обоих случаях.

случай (E) определяется законами (1) и (2) монады:

-- apply (1) to (B (Just (P y1 y2)))
join (return' (B (Just (P y1 y2))))
= -- using our definition of return'
join (B (Just (P (B (Just (P y1 y2))) (B (Just (P y1 y2))))))
= -- from (1) this should equal
B (Just (P y1 y2))

для того, чтобы вернуть B (Just (P y1 y2)) в случае (E), это означает, что мы должны выбрать y1 либо x1 или x3, и y2 либо x2 или x4.

-- apply (2) to (B (Just (P y1 y2)))
join (fmap return' (B (Just (P y1 y2))))
= -- def of fmap
join (B (Just (P (return y1) (return y2))))
= -- def of return
join (B (Just (P (B (Just (P y1 y1))) (B (Just (P y2 y2))))))
= -- from (2) this should equal
B (Just (P y1 y2))

точно так же, это говорит о том, что мы должны выбрать y1 либо x1 или x2 и y2 от любого x3 или x4. Объединение двух, мы определяем, что правая сторона (E) должна быть B (Just (P x1 x4)).

пока все хорошо, но проблема возникает, когда вы пытаетесь заполнить правые стороны для (C) и (D).

есть 5 возможных правых сторон для каждого, и ни одна из комбинаций не работает. У меня пока нет хорошего аргумента для этого, но у меня есть программа, которая исчерпывающе проверяет все комбинации:

{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables #-}

import Control.Monad (guard)

data Pair a = P a a
  deriving (Eq, Show)

instance Functor Pair where
  fmap f (P x y) = P (f x) (f y)

instance Monad Pair where
  return x = P x x
  P a b >>= f = P x y
    where P x _ = f a
          P _ y = f b

newtype Bad a = B (Maybe (Pair a))
  deriving (Eq, Show)

instance Functor Bad where
  fmap f (B x) = B $ fmap (fmap f) x

-- The only definition that could possibly work.
unit :: a -> Bad a
unit x = B (Just (P x x))

-- Number of possible definitions of join for this type. If this equals zero, no monad for you!
joins :: Integer
joins = sum $ do
  -- Try all possible ways of handling cases 3 and 4 in the definition of join below.
  let ways = [ \_ _ -> B Nothing
             , \a b -> B (Just (P a a))
             , \a b -> B (Just (P a b))
             , \a b -> B (Just (P b a))
             , \a b -> B (Just (P b b)) ] :: [forall a. a -> a -> Bad a]
  c3 :: forall a. a -> a -> Bad a <- ways
  c4 :: forall a. a -> a -> Bad a <- ways

  let join :: forall a. Bad (Bad a) -> Bad a
      join (B Nothing) = B Nothing -- no choice
      join (B (Just (P (B Nothing) (B Nothing)))) = B Nothing -- again, no choice
      join (B (Just (P (B (Just (P x1 x2))) (B Nothing)))) = c3 x1 x2
      join (B (Just (P (B Nothing) (B (Just (P x3 x4)))))) = c4 x3 x4
      join (B (Just (P (B (Just (P x1 x2))) (B (Just (P x3 x4)))))) = B (Just (P x1 x4)) -- derived from monad laws

  -- We've already learnt all we can from these two, but I decided to leave them in anyway.
  guard $ all (\x -> join (unit x) == x) bad1
  guard $ all (\x -> join (fmap unit x) == x) bad1

  -- This is the one that matters
  guard $ all (\x -> join (join x) == join (fmap join x)) bad3

  return 1 

main = putStrLn $ show joins ++ " combinations work."

-- Functions for making all the different forms of Bad values containing distinct Ints.

bad1 :: [Bad Int]
bad1 = map fst (bad1' 1)

bad3 :: [Bad (Bad (Bad Int))]
bad3 = map fst (bad3' 1)

bad1' :: Int -> [(Bad Int, Int)]
bad1' n = [(B Nothing, n), (B (Just (P n (n+1))), n+2)]

bad2' :: Int -> [(Bad (Bad Int), Int)]
bad2' n = (B Nothing, n) : do
  (x, n')  <- bad1' n
  (y, n'') <- bad1' n'
  return (B (Just (P x y)), n'')

bad3' :: Int -> [(Bad (Bad (Bad Int)), Int)]
bad3' n = (B Nothing, n) : do
  (x, n')  <- bad2' n
  (y, n'') <- bad2' n'
  return (B (Just (P x y)), n'')

для небольшого конкретного контрпримера рассмотрим терминальную монаду.

data Thud x = Thud

The return и >>= просто иди Thud, а законы держатся тривиально.

теперь давайте также иметь монаду писателя для Bool (с, скажем, структурой xor-моноида).

data Flip x = Flip Bool x

instance Monad Flip where
   return x = Flip False x
   Flip False x  >>= f = f x
   Flip True x   >>= f = Flip (not b) y where Flip b y = f x

Эм, нам понадобится композиция

newtype (:.:) f g x = C (f (g x))

теперь попробуем определить...

instance Monad (Flip :.: Thud) where  -- that's effectively the constant `Bool` functor
  return x = C (Flip ??? Thud)
  ...

Параметричность говорит нам, что ??? не может зависеть от любого полезного способа x, так что это должна быть константа. В результате join . return также обязательно является постоянной функцией, следовательно, закон

join . return = id

должен потерпеть неудачу для любых определений join и return мы выбираем.

строительство исключенного третьего

(->) r - это монада для каждого r и Either e - это монада для каждого e. Определим их состав ((->) r внутри Either e наружу):

import Control.Monad
newtype Comp r e a = Comp { uncomp :: Either e (r -> a) }

я утверждаю, что если Comp r e были монады для каждого r и e тогда мы могли бы понять закон исключенного среднего. Это невозможно в интуиционистской логики который лежит в основе типовых систем функциональные языки (наличие закона исключенного среднего эквивалентно наличию call / cc оператор).

предположим Comp - это монада. Тогда у нас есть

join :: Comp r e (Comp r e a) -> Comp r e a

и поэтому мы можем определить

swap :: (r -> Either e a) -> Either e (r -> a)
swap = uncomp . join . Comp . return . liftM (Comp . liftM return)

(это просто swap функция из бумаги сочинения монады что Брент упоминает, секта. 4.3, только с добавлением конструкторов newtype (de). Обратите внимание, что нам все равно, какие свойства он имеет, единственное, что важно разве что она определима и тотальна.)

теперь давайте установим

data False -- an empty datatype corresponding to logical false
type Neg a = (a -> False) -- corresponds to logical negation

и специализировать своп для r = b,e = b,a = False:

excludedMiddle :: Either b (Neg b)
excludedMiddle = swap Left

вывод: хотя (->) r и Either r это монады, их состав Comp r r не может быть.

Примечание: это также отражено в how ReaderT и EitherT определены. иReaderT r (Either e) и EitherT e (Reader r) изоморфны r -> Either e a! Нет никакого способа, как определить монаду для двойной Either e (r -> a).


побег IO действия

есть много примеров в том же ключе, что привлекать IO и которые ведут к побегу IO как-то. Например:

newtype Comp r a = Comp { uncomp :: IO (r -> a) }

swap :: (r -> IO a) -> IO (r -> a)
swap = uncomp . join . Comp . return . liftM (Comp . liftM return)

теперь

main :: IO ()
main = do
   let foo True  = print "First" >> return 1
       foo False = print "Second" >> return 2
   f <- swap foo
   input <- readLn
   print (f input)

что произойдет при запуске этой программы? Есть две возможности:

  1. печатается"первый" или "второй"после мы читаем input из консоли, что означает, что последовательность действий была отменено и что за действия от foo сбежал в чистую f.
  2. или swap (отсюда join) выбросит IO действие и ни "первый", ни "второй" никогда не печатается. Но это значит, что join нарушает закон

    join . return = id
    

    потому что если join выдает IO акции, тогда

    foo ≠ (join . return) foo
    

другое подобное IO + комбинации монад приводят к построению

swapEither :: IO (Either e a) -> Either e (IO a)
swapWriter :: (Monoid e) => IO (Writer e a) -> Writer e (IO a)
swapState  :: IO (State e a) -> State e (IO a)
...

либо join реализации должны позволить e спасаясь от IO или они должны выбросить и заменить чем-то другим, нарушая закон.

ваша ссылка ссылается на этот тип данных, поэтому давайте попробуем выбрать какую-то конкретную реализацию: data A3 a = A3 (A1 (A2 a))

Я буду произвольно выбирать A1 = IO, A2 = []. Мы также сделаем это newtype и дать ему особенно острое имя, для удовольствия:

newtype ListT IO a = ListT (IO [a])

давайте придумаем какое-нибудь произвольное действие в этом типе и запустим его двумя разными, но равными способами:

λ> let v n = ListT $ do {putStr (show n); return [0, 1]}
λ> runListT $ ((v >=> v) >=> v) 0
0010101[0,1,0,1,0,1,0,1]
λ> runListT $ (v >=> (v >=> v)) 0
0001101[0,1,0,1,0,1,0,1]

как видите, это нарушает закон ассоциативности:∀x y z. (x >=> y) >=> z == x >=> (y >=> z).

получается вон, ListT m это только монада, если m это коммутативной монады. Это предотвращает большую категорию монад от сочинения с [], что нарушает универсальное правило "составление двух произвольных монад дает монаду".

Смотрите также:https://stackoverflow.com/a/12617918/1769569