Jak działa wyrażenie `ap zip tail`?

Question

Zastanawiałem się, jak napisać f x = zip x (tail x) w punkcie wolnym. Użyłem programu pointfree, a wynikiem było f = ap zip tail. ap funkcja od Control.Monad

Nie rozumiem, jak działa punktowa definicja. Mam nadzieję, że uda mi się to rozgryźć, jeśli potrafię to zrozumieć z perspektywy typów.

import Control.Monad (ap) 
let f = ap zip tail 
let g = ap zip 
:info ap zip tail f g 
ap :: Monad m => m (a -> b) -> m a -> m b 
    -- Defined in `Control.Monad' 
zip :: [a] -> [b] -> [(a, b)] -- Defined in `GHC.List' 
tail :: [a] -> [a]  -- Defined in `GHC.List' 
f :: [b] -> [(b, b)] -- Defined at <interactive>:3:5 
g :: ([a] -> [b]) -> [a] -> [(a, b)] 
    -- Defined at <interactive>:4:5 

Patrząc na wypowiedzi ap zip tail Myślę, że zamek błyskawiczny jest pierwszym parametrem ap i ogona jest drugim parametrem ap.

Monad m => m (a -> b) -> m a -> m b 
      \--------/ \---/ 
       zip  tail 

Ale nie jest to możliwe, ponieważ rodzaje zip i tail są zupełnie inne niż to, co funkcja ap wymaga. Nawet biorąc pod uwagę, że lista jest monadą.

Answer 1

Zatem sygnatura typu ap to Monad m => m (a -> b) -> m a -> m b. Podałeś jako argumenty zip i tail, spójrzmy więc na ich sygnatury typu.

Począwszy tail :: [a] -> [a] ~ (->) [a] [a] (tutaj ~ jest operator równości na typy), jeśli porównamy ten rodzaj przeciw typu drugiego argumentu dla ap,

(->) [x] [x] ~ m a 
((->) [x]) [x] ~ m a 

otrzymujemy a ~ [x] i m ~ ((->) [x]) ~ ((->) a). Już teraz widzimy, że monada, w której się znajdujemy, to (->) [x], a nie []. Jeżeli podstawimy co możemy do podpisu typu ap otrzymujemy:

(((->) [x]) ([x] -> b)) -> (((->) [x]) [x]) -> (((->) [x]) b) 

Ponieważ nie jest bardzo czytelny, nie może być bardziej normalnie zapisać jako

([x] -> ([x] -> b)) -> ([x] -> [x]) -> ([x] -> b) 
~ ([x] -> [x] -> b) -> ([x] -> [x]) -> ([x] -> b) 

Rodzaj zip jest [x] -> [y] -> [(x, y)]. Już teraz widać, że to zrówna się z pierwszym argumentem ap gdzie

[x]   ~ [x] 
[y]   ~ [x] 
[(x, y)] ~ b 

Tutaj mam wymienione typy pionowo, dzięki czemu można łatwo sprawdzić, które rodzaje linii. Tak oczywiście x ~ x, y ~ x i [(x, y)] ~ [(x, x)] ~ b, więc możemy skończyć zastępując b ~ [(x, x)] do typu podpisu ap „s i dostać

([x] -> [x] -> [(x, x)]) -> ([x] -> [x]) -> ([x] -> [(x, x)]) 
-- zip      tail  (ap zip tail) 
--           ap zip tail u = zip u (tail u) 

Mam nadzieję, że czyści rzeczy dla Ciebie.

EDIT: Jak danvaripointed out w komentarzach, monada (->) a jest czasami nazywany Monada czytelnika.

Answer 2

Istnieją dwa aspekty do zrozumienia tego:

1. typu magia
2. Przepływ informacji o wdrażaniu

Po pierwsze, to pomogło mi zrozumieć typu magicznego:

1) zip   : [a] → ([a] → [(a,a)]) 
2) tail   : [a] → [a] 
3) zip <*> tail : [a] → [(a,a)] 

4) <*> : Applicative f ⇒ f (p → q) → f p → f q 

W tym Sprawa dla <*>,

5) f x = y → x 

Należy zauważyć, że w 5, f jest konstruktorem typu. Zastosowanie f do x powoduje utworzenie typu. Również tutaj = jest przeciążone, aby określić równoważność typów.

y to obecnie miejsce Uchwyt w tym przypadku jest to [a], co oznacza

6) f x = [a] -> x 

stosując 6, można przepisać 1,2 i 3, jak następuje:

7) zip   : f ([a] → [(a,a)]) 
8) tail   : f [a] 
9) zip <*> tail : f ([a] → [(a,a)]) → f [a] → f [(a,a)] 

Patrząc na 4, zastępujemy:

10) p = [a] 
11) q = [(a,a)] 
12) f x = [a] → x 

(Powtórzenie 6 tutaj ponownie jako 12)

Po drugie, przepływ informacji , tj. rzeczywista funkcjonalność. Jest to łatwiejsze, jak wynika z definicji <*> dla Applicative instance of y →, który jest przepisany tutaj z różnymi nazwami identyfikator i używając stylu Infix:

13) g <*> h $ xs = g xs (h xs) 

zastępująca następująco:

14) g = zip 
15) h = tail 

Daje:

zip <*> tail $ xs  (Using 14 and 15) 
    == 
zip xs (tail xs)   (Using 13)