Zachowanie odwrocie >> = (==)

Question

Funkcja dla określenia, czy ciąg jest palindrom mogą być realizowane w pointfree aplikacyjnej sposób poprzez

pal1 = (==) <$> reverse <*> id 

A oto monadycznego wersja

reverse >>= (==) 

Jak działa wersja modadic bez wyraźnego wywołania id? Próbowałem oglądać reprezentację poinful za pomocą pointful i odzyskać tę samą funkcję.

Answer 1

Działa to na podstawie faktu, że x -> y można uznać za swego rodzaju "monadę czytelnika". Jeśli mielibyśmy powiedzieć:

type Reader r x = r -> x 

to mamy instancję Monad (Reader r). Tak więc widzimy, że

reverse :: [x] -> [x] 

jest rzeczywiście

reverse :: Reader [x] [x] 

Podobnie

(==) :: [x] -> [x] -> Bool 

można zapisać jako

(==) :: [x] -> Reader [x] Bool 

Następnie (>>=) łączy dwie razem.

Więc ... Zaczynamy od reverse, która jest czynnością Reader, która odczytuje listę i zwraca listę. Następnie używamy >>=, aby przekazać to do ==, która jest funkcją, która pobiera listę, i zwraca Reader [x] Bool.

W skrócie, lista wejściowa jest powielana przez akcję Reader, która zasadniczo pobiera dane wejściowe i przekazuje je do każdej funkcji w łańcuchu. (To co monada czytelnik jest.)

Mam nadzieję, że popełnił jakiś sens ... Zajęło me chwilę, aby dowiedzieć się!

Answer 2

Rzućmy okiem na przykład Monad dla ((->) r):

instance Monad ((->) r) where 
    return = const 
    f >>= k = \ r -> k (f r) r 

a następnie po prostu podać kod monadycznej:

reverse >>= (==) = \r -> (==) (reverse r) r 

które możemy napisać w bardziej znany sposób:

\r -> reverse r == r 

Answer 3

Aby dodać do innych odpowiedzi, oto kolejny POV na ten temat. Weźmy definicji wiążą poprzez fmap i join:

m >>= act = join (fmap act m) 

Wyrażenie (==) <$> reverse ma typ Eq a => [a] -> [a] -> Bool i odpowiada fmap (==) reverse.Teraz przekazujemy go do join :: m (m a) -> m a, a dla instancji monad (->) r typem będzie ([a] -> [a] -> Bool) -> ([a] -> Bool). Oznacza to, że join jest dokładnie częścią <*> id.

Answer 4

Myślę, że najprostszym sposobem, aby zrozumieć to patrząc na typy:

(>>=) :: Monad m => m a -> (a -> m b) -> m b 

wyspecjalizowanym do instancji ((->) r):

(>>=) :: (r -> a) -> (a -> r -> b) -> r -> b 

Nie podano e a. Jedynym sposobem na jego wytworzenie jest zastosowanie pierwszej funkcji r -> a do podanej przez ciebie r. Jedynym sposobem na wyprodukowanie b jest zastosowanie drugiej funkcji do właśnie wyprodukowanej r i. Oznacza to, że jedyną możliwą definicję tej funkcji ^* jest:

f >>= g = \a -> g (f a) a 

Podłączenie nasze argumenty, otrzymujemy:

reverse >>= (==) 

-- definition of (>>=) 
= \a -> (==) (reverse a) a 

-- prefix to infix 
= \a -> reverse a == a 

Parametricity jest potężnym narzędziem do wnioskowania o funkcji polimorficznych.

---

* inny niż dolnej

Answer 5

innych odpowiedzi potwierdzają, że dwa zachowują się tak samo, ale nie wyjaśniają, gdzie id faktycznie poszedł. W tej odpowiedzi spróbuję to zrobić. Punchlina jest taka, że ​​dla Readera mamy ciekawy -wyjęcie równania: id >>= return . f = f. (Bardziej piękna forma tego równania to: (id >>=) = (>>= id); wraz z prawami monady piękna forma oznacza łatwą do wykorzystania formę). Aby wyjaśnić nieco prostsze, zamiast próbować przekształcić z formy aplikacyjnej w formę monadyczną, po prostu przyjąć za pewnik, że wierzysz następujące równanie:

(==) <$> reverse <*> id 
= { too annoying to do carefully } 
reverse >>= \xs -> id >>= \ys -> return ((==) xs ys) 

Więc zaczniemy od tej ostatniej linii, a kończy na reverse >>= (==). Po drodze będzie kluczem do zauważenia, że ​​id jest tożsamością dla (.) - która tak się akurat okazała być fmap dla monitory Reader. Oto:

reverse >>= \xs -> id >>= \ys -> return ((==) xs ys) 
= { monad law } 
reverse >>= \xs -> fmap ((==) xs) id 
= { definition of fmap for Reader } 
reverse >>= \xs -> (.) ((==) xs) id 
= { id is the identity of fmap } 
reverse >>= \xs -> (==) xs 
= { eta reduction } 
reverse >>= (==) 

Jakie jest znaczenie id >>= return . f = f? Cóż, traktując funkcje jako "wartości indeksowane", możemy zrozumieć, że id jest wartością równą jej indeksowi; i return jako wartość, która wszędzie jest taka sama. Więc id >>= return . f mówi „patrzeć na indeks x; następnie, (wciąż w indeksie x) zwraca wartość, która ignoruje jej indeks i ma wartość f x”. Tak się składa, że ​​indeks ignorować, a wartość możemy oddać do f meczu up - więc równie dobrze możemy pominąć cały ten zadnie i po prostu powiedzieć „spojrzeć na indeks x i zastosować f do niego”. To jest znaczenie równania.