Powszechnie wiadomo, że funktory aplikacyjne są zamknięte w kompozycji, ale monady nie. Jednak mam problem ze znalezieniem konkretnego kontrprzykładu pokazującego, że monady nie zawsze komponują.
Ta odpowiedź daje [String -> a]
jako przykład nie-monady. Po trochę zabawie z tym, wierzę w to intuicyjnie, ale ta odpowiedź mówi tylko, że „złączenia nie można zaimplementować” bez podania żadnego uzasadnienia. Chciałbym coś bardziej formalnego. Oczywiście istnieje wiele funkcji z typem [String -> [String -> a]] -> [String -> a]
; trzeba wykazać, że jakakolwiek taka funkcja niekoniecznie spełnia prawa monady.
Dowolny przykład (z towarzyszącym dowodem) wystarczy; Niekoniecznie szukam w szczególności dowodu na powyższy przykład.
haskell
monads
composition
proof
Brent Yorgey
źródło
źródło
join
dla kompozycji dwóch monad w ogólne . Ale to nie prowadzi do żadnych konkretnych przykładów.Odpowiedzi:
Rozważ tę monadę, która jest izomorficzna z
(Bool ->)
monadą: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
i skomponuj go z
Maybe
monadą:newtype Bad a = B (Maybe (Pair a))
Twierdzę, że
Bad
to nie może być monada.Częściowy dowód:
Jest tylko jeden sposób, aby określić
fmap
, który spełniafmap id = id
:instance Functor Bad where fmap f (B x) = B $ fmap (fmap f) x
Przypomnij sobie prawa monady:
(1) join (return x) = x (2) join (fmap return x) = x (3) join (join x) = join (fmap join x)
Aby zdefiniować
return x
, mamy dwie możliwości:B Nothing
lubB (Just (P x x))
. Jest jasne, że aby mieć jakąkolwiek nadzieję na powrótx
z (1) i (2), nie możemy wyrzucićx
, więc musimy wybrać drugą opcję.return' :: a -> Bad a return' x = B (Just (P x x))
To odchodzi
join
. Ponieważ istnieje tylko kilka możliwych danych wejściowych, możemy przedstawić przypadek dla każdego: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)))))) = ???
Ponieważ dane wyjściowe mają typ
Bad a
, jedyne opcje toB Nothing
lubB (Just (P y1 y2))
gdziey1
,y2
należy wybrać spośródx1 ... x4
.W przypadkach (A) i (B) nie mamy wartości typu
a
, więcB Nothing
w obu przypadkach jesteśmy zmuszeni do zwrócenia .Przypadek (E) jest określony przez prawa monady (1) i (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))
Aby powrócić
B (Just (P y1 y2))
w przypadku (E), oznacza to, że musimy wybraćy1
albox1
albox3
,y2
albox2
albo albo albox4
.-- 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))
To samo mówi, że musimy wybierać
y1
spośród albox1
albox2
, albo , albo ,y2
albo,x3
albox4
. Łącząc oba, ustalamy, że prawa strona (E) musi byćB (Just (P x1 x4))
.Jak dotąd wszystko jest w porządku, ale problem pojawia się, gdy próbujesz wypełnić prawe strony dla (C) i (D).
Istnieje 5 możliwych prawych stron dla każdej i żadna z kombinacji nie działa. Nie mam jeszcze na to ładnego argumentu, ale mam program, który wyczerpująco testuje wszystkie kombinacje:
{-# 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'')
źródło
swap :: Pair (Maybe a) -> Maybe (Pair a)
.(Maybe a, Maybe a)
jest monadą (ponieważ jest produktem dwóch monad), aleMaybe (a, a)
nie jest monadą. Potwierdziłem również, żeMaybe (a,a)
nie jest to monada przez wyraźne obliczenia.Maybe (a, a)
nie jest monadą? Obie opcje, może i krotka, są przemienne i powinny być tworzone w dowolnej kolejności; istnieją inne pytania SO, które również dotyczą tego konkretnego przykładu.Dla małego konkretnego kontrprzykładu rozważmy monadę terminalu.
data Thud x = Thud
return
I>>=
po prostu pójśćThud
, a prawa trzymać trywialnie.Weźmy teraz również monadę pisarza dla Bool (z, powiedzmy, strukturą xor-monoid).
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
Eee, potrzebujemy kompozycji
newtype (:.:) f g x = C (f (g x))
Teraz spróbuj zdefiniować ...
instance Monad (Flip :.: Thud) where -- that's effectively the constant `Bool` functor return x = C (Flip ??? Thud) ...
Parametryczność mówi nam, że
???
nie można od nich w żaden użyteczny sposób polegaćx
, więc musi być stałą. W rezultaciejoin . return
jest z konieczności również funkcją stałą, stąd prawojoin . return = id
musi zawieść dla jakichkolwiek definicji
join
ireturn
wybierzemy.źródło
Konstruowanie wykluczonego środka
(->) r
jest monadą dla każdegor
iEither e
jest monadą dla każdegoe
. Określmy ich skład ((->) r
wewnątrz, naEither e
zewnątrz):import Control.Monad newtype Comp r e a = Comp { uncomp :: Either e (r -> a) }
I twierdzą, że jeśli
Comp r e
były monada dla każdegor
ie
wtedy moglibyśmy zrealizować prawo nieobecny środku . Nie jest to możliwe w logice intuicjonistycznej, która leży u podstaw typosystemów języków funkcyjnych (posiadanie prawa wyłączonego środka jest równoznaczne z posiadaniem operatora wywołania / cc ).Załóżmy, że
Comp
jest to monada. Potem będziejoin :: Comp r e (Comp r e a) -> Comp r e a
i tak możemy zdefiniować
swap :: (r -> Either e a) -> Either e (r -> a) swap = uncomp . join . Comp . return . liftM (Comp . liftM return)
(To tylko
swap
funkcja z artykułu Tworzenie monad, o których wspomina Brent, sekcja 4.3, tylko z dodanymi (de) konstruktorami newtype. Zauważ, że nie obchodzi nas, jakie ma właściwości, jedyną ważną rzeczą jest to, że jest definiowalna i całkowita .)Teraz zaczynajmy
data False -- an empty datatype corresponding to logical false type Neg a = (a -> False) -- corresponds to logical negation
i specjalizuje się na zamianę
r = b
,e = b
,a = False
:excludedMiddle :: Either b (Neg b) excludedMiddle = swap Left
Wniosek: chociaż są
(->) r
iEither r
są monadami, ich składComp r r
nie może być.Uwaga: znajduje to również odzwierciedlenie w sposobie
ReaderT
i sposobieEitherT
definiowania. ZarównoReaderT r (Either e)
iEitherT e (Reader r)
jest izomorficznar -> Either e a
! Nie ma sposobu, jak zdefiniować monadę dla dualnościEither e (r -> a)
.IO
Działania ucieczkiJest wiele przykładów w tym samym duchu, które obejmują
IO
i prowadzą do ucieczkiIO
. Na przykład: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)
A teraz miejmy
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)
Co się stanie, gdy ten program zostanie uruchomiony? Istnieją dwie możliwości:
input
z konsoli, co oznacza, że sekwencja działań został odwrócony i że działania odfoo
uciekł do czystaf
.Lub
swap
(stądjoin
) odrzucaIO
akcję i ani „Pierwszy”, ani „Drugi” nigdy nie są drukowane. Ale to oznacza, żejoin
narusza prawojoin . return = id
ponieważ jeśli
join
odrzucaIO
działanie, tofoo ≠ (join . return) foo
Inne podobne
IO
kombinacje + monada prowadzą do konstruowaniaswapEither :: 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) ...
Albo ich
join
implementacje muszą pozwoliće
na ucieczkę,IO
albo muszą to wyrzucić i zastąpić czymś innym, łamiącym prawo.źródło
<*>
zamiast tego), próbowałem go edytować, ale powiedziano mi, że moja edycja jest za krótka.) --- Nie jest jasne, czy mnie, że posiadanie definicji dlajoin
implikuje definicję dlaswap
. Czy mógłbyś to rozwinąć? Artykuł, do którego odnosi się Brent wydaje się sugerować, że aby przejść odjoin
doswap
potrzebujemy następujących założeń:joinM . fmapM join = join . joinM
ijoin . fmap (fmapM joinN ) = fmapM joinN . join
gdzie joinM = join :: M itd.swap
na pasującą do papieru). Do tej pory nie sprawdzałem papieru i masz rację, wygląda na to, że potrzebujemy J (1) i J (2) do zdefiniowaniaswap
<->join
. To chyba słaby punkt mojego dowodu i pomyślę o tym więcej (może dałoby się coś wyciągnąć z tego, że jestApplicative
).join
, moglibyśmy zdefiniowaćswap :: (Int -> Maybe a) -> Maybe (Int -> a)
za pomocą powyższej definicji (bez względu na to, jakie prawa toswap
spełnia). Jak taki by sięswap
zachowywał? Ponieważ nieInt
, nie ma nic do przekazania do swojego argumentu, więc musiałby zwrócićNothing
wszystkie dane wejściowe. Wierzę, że możemy uzyskać sprzeczność zjoin
prawami monady bez konieczności definiowania ichjoin
odswap
tyłu. Sprawdzę to i dam znać.Twoje łącze odnosi się do tego typu danych, więc spróbujmy wybrać konkretną implementację:
data A3 a = A3 (A1 (A2 a))
Samowolnie wybiorę
A1 = IO, A2 = []
. Zrobimy też tonewtype
i nadamy mu szczególnie spiczastą nazwę, dla zabawy:newtype ListT IO a = ListT (IO [a])
Wymyślmy dowolną akcję tego typu i uruchommy ją na dwa różne, ale równe sposoby:
λ> 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]
Jak widać, to łamie prawo skojarzeń:
∀x y z. (x >=> y) >=> z == x >=> (y >=> z)
.Okazuje się, że
ListT m
jest monadą tylko wtedy, gdym
jest monadą przemienną . Uniemożliwia to komponowanie dużej kategorii monad[]
, co łamie uniwersalną zasadę, że „komponowanie dwóch dowolnych monad daje monadę”.Zobacz też: https://stackoverflow.com/a/12617918/1769569
źródło
ListT
nie tworzy monady we wszystkich przypadkach, a nie pokazuje, że żadna możliwa definicja nie zadziała.Monad
instancja dlaListT
i wykazanie, że nie ma innych. Stwierdzenie brzmi: „dla tego wszystkiego istnieje tamto”, a więc zaprzeczeniem jest „istnieje to, co dla tego wszystkiego”Monady nie komponują. Nie w sposób ogólny - nie ma ogólnego sposobu komponowania monad. Zobacz https://www.slideshare.net/pjschwarz/monads-do-not-compose
źródło