Wnioskodawcy tworzą, monady nie

Wnioskodawcy tworzą, monady nie.

Co oznacza powyższe stwierdzenie? A kiedy jedno jest lepsze od drugiego?

Jeśli porównamy typy

(<*>) :: Applicative a => a (s -> t) -> a s -> a t
(>>=) :: Monad m =>       m s -> (s -> m t) -> m t

otrzymujemy wskazówkę, co oddziela te dwa pojęcia. To (s -> m t)w typie (>>=)pokazuje, że wartość w smoże określać zachowanie obliczenia w m t. Monady pozwalają na interferencję między warstwami wartości i obliczeń. (<*>)Operator nie umożliwia takich zakłóceń: Działanie i argumentów obliczenia nie zależy od wartości. To naprawdę gryzie. Porównać

miffy :: Monad m => m Bool -> m x -> m x -> m x
miffy mb mt mf = do
  b <- mb
  if b then mt else mf

który wykorzystuje wynik jakiegoś efektu do wyboru między dwoma obliczeniami (np. wystrzelenie rakiet i podpisanie rozejmu), podczas gdy

iffy :: Applicative a => a Bool -> a x -> a x -> a x
iffy ab at af = pure cond <*> ab <*> at <*> af where
  cond b t f = if b then t else f

która używa wartości abdo wyboru między wartościami dwóch obliczeń ati af, po przeprowadzeniu obu, być może z tragicznym skutkiem.

Wersja monadyczna polega zasadniczo na dodatkowej mocy (>>=)wyboru obliczeń z wartości, a to może być ważne. Jednak wspieranie tej mocy utrudnia komponowanie monad. Jeśli spróbujemy zbudować „podwójne wiązanie”

(>>>>==) :: (Monad m, Monad n) => m (n s) -> (s -> m (n t)) -> m (n t)
mns >>>>== f = mns >>-{-m-} \ ns -> let nmnt = ns >>= (return . f) in ???

dotarliśmy tak daleko, ale teraz wszystkie nasze warstwy są pomieszane. Mamy n (m (n t)), więc musimy pozbyć się zewnętrznego n. Jak mówi Alexandre C, możemy to zrobić, jeśli mamy odpowiedni

swap :: n (m t) -> m (n t)

permutować do nwewnątrz i joindo drugiego n.

Słabsze „podwójne zastosowanie” jest znacznie łatwiejsze do zdefiniowania

(<<**>>) :: (Applicative a, Applicative b) => a (b (s -> t)) -> a (b s) -> a (b t)
abf <<**>> abs = pure (<*>) <*> abf <*> abs

ponieważ nie ma interferencji między warstwami.

W związku z tym dobrze jest rozpoznać, kiedy naprawdę potrzebujesz dodatkowej mocy Monads i kiedy możesz uciec ze sztywną strukturą obliczeniową, która Applicativeobsługuje.

Zwróć uwagę, że chociaż komponowanie monad jest trudne, może to być więcej niż potrzebujesz. Typ m (n v)wskazuje na obliczanie z m-efektami, a następnie obliczanie z n-efekty do -wartości v, gdzie m-efekty kończą się przed nrozpoczęciem -efekty (stąd potrzeba swap). Jeśli chcesz po prostu przeplatać m-efekty z n-efektami, to o skład może zbyt wiele prosić!

Wnioskodawcy tworzą, monady nie.

Monady zrobić komponować, ale wynik może nie być monada. W przeciwieństwie do tego kompozycja dwóch aplikantów jest z konieczności aplikatywna. Podejrzewam, że intencją pierwotnego stwierdzenia było to, że „Aplikacyjność komponuje, a monadność nie”. Ponownie, „ Applicativejest zamknięty w kompozycji, a Monadnie jest”.

Jeśli masz aplikacje A1i A2, to typ data A3 a = A3 (A1 (A2 a))też jest aplikacyjny (możesz napisać taką instancję w sposób ogólny).

Z drugiej strony, jeśli masz monady M1i M2typ data M3 a = M3 (M1 (M2 a))niekoniecznie jest monadą (nie ma sensownej ogólnej implementacji dla >>=lub joindla kompozycji).

Jednym z przykładów może być typu [Int -> a](tu skomponować konstruktora typu []z (->) Int, z których oba są monady). Możesz łatwo pisać

app :: [Int -> (a -> b)] -> [Int -> a] -> [Int -> b]
app f x = (<*>) <$> f <*> x

I to uogólnia na każdą aplikację:

app :: (Applicative f, Applicative f1) => f (f1 (a -> b)) -> f (f1 a) -> f (f1 b)

Ale nie ma sensownej definicji

join :: [Int -> [Int -> a]] -> [Int -> a]

Jeśli nie jesteś tego przekonany, rozważ następujące wyrażenie:

join [\x -> replicate x (const ())]

Długość zwracanej listy musi być ustawiona w kamieniu przed podaniem liczby całkowitej, ale prawidłowa jej długość zależy od podanej liczby całkowitej. Dlatego nie joinmoże istnieć żadna poprawna funkcja dla tego typu.

Niestety nasz prawdziwy cel, czyli kompozycja monad, jest raczej trudniejszy. .. W rzeczywistości możemy faktycznie udowodnić, że w pewnym sensie nie ma sposobu, aby skonstruować funkcję złączenia z powyższym typem, używając tylko operacji dwóch monad (patrz załącznik, aby zapoznać się z zarysem dowodu). Wynika z tego, że jedyny sposób, w jaki możemy mieć nadzieję na utworzenie kompozycji, to istnienie dodatkowych konstrukcji łączących te dwa składniki.

Komponowanie monad, http://web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf

Rozwiązanie prawa dystrybucji l: MN -> NM jest wystarczające

aby zagwarantować monadyczność NM. Aby to zobaczyć, potrzebujesz jednostki i wielu. skoncentruję się na mnogości (jednostka to jednostka_N jednostka M)

NMNM - l -> NNMM - mult_N mult_M -> NM

Ten sposób nie gwarantuje, że MN jest monada.

Kluczowa obserwacja pojawia się jednak, gdy masz rozwiązania prawa dystrybucyjnego

l1 : ML -> LM
l2 : NL -> LN
l3 : NM -> MN

zatem LM, LN i MN są monadami. Powstaje pytanie, czy LMN jest monadą (albo wg

(MN) L -> L (MN) lub przez N (LM) -> (LM) N

Mamy wystarczającą strukturę, aby stworzyć te mapy. Jednak, jak zauważa Eugenia Cheng , potrzebujemy warunku heksagonalnego (który sprowadza się do przedstawienia równania Yanga-Baxtera), aby zagwarantować monadyczność obu konstrukcji. W rzeczywistości, przy warunku heksagonalnym, dwie różne monady pokrywają się.