Как работает выражение `ap zip tail`

Я задавался вопросом, как написать f x = zip x (tail x) в точке бесплатно. Таким образом, я использовал программу pointfree, и результат был f = ap zip tail. ap является функцией из Control.Monad

Я не понимаю, как работает свободное определение точки. Надеюсь, я смогу понять это, если смогу понять это с точки зрения типов.

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

Посмотрев на выражение ap zip tail, я думаю, что zip является первым параметром ap, а tail - вторым параметром ap.

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

Но это невозможно, потому что типы zip и tail полностью отличаются от того, что требует функция ap. Даже с учетом того, что список является монадой.

Ответы

Ответ 1

Таким образом, сигнатура типа ap равна Monad m => m (a -> b) -> m a -> m b. Вы дали ему zip и tail в качестве аргументов, поэтому давайте посмотрим на их сигнатуры типов.

Начиная с tail :: [a] -> [a] ~ (->) [a] [a] (здесь ~ - оператор равенства для типов), если мы сравниваем этот тип с типом второго аргумента для ap,

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

получаем a ~ [x] и m ~ ((->) [x]) ~ ((->) a). Уже мы видим, что монада, в которой мы находимся, (->) [x], а не []. Если мы подставим то, что можем, в сигнатуру типа ap, получим:

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

Так как это не очень читаемо, его можно более обычно записывать как

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

Тип zip - [x] -> [y] -> [(x, y)]. Мы уже можем видеть, что это соответствует первому аргументу ap, где

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

Здесь я перечислил типы по вертикали, чтобы вы могли легко видеть, какие типы выстраиваются в линию. Очевидно, что x ~ x, y ~ x и [(x, y)] ~ [(x, x)] ~ b, поэтому мы можем закончить замену b ~ [(x, x)] на подпись типа ap и получить

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

Я надеюсь, что это очистит вас.

EDIT: danvari отметил в комментариях, монада (->) a иногда называется монадой читателя.

Ответ 2

Есть два аспекта для понимания этого:

  • Тип магии
  • Информационный поток реализации

Во-первых, это помогло мне понять магию типа:

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

В этом случае для <*>,

5) f x = y → x

Обратите внимание, что в 5, f является конструктором типа. Применение f to x создает тип. Кроме того, здесь = перегружается до средней эквивалентности типов.

y в настоящее время является держателем места, в этом случае это [a], что означает

6) f x = [a] -> x

Используя 6, мы можем переписать 1,2 и 3 следующим образом:

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

Итак, глядя на 4, мы подставляем следующее:

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

(Повторение 6 здесь снова как 12)

Во-вторых, поток информации, то есть фактическая функциональность. Это проще, из определения <*> видно, что Аппликативный экземпляр y →, который переписывается здесь с разными именами идентификаторов и с использованием стиля infix:

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

Подставляя следующее:

14) g = zip
15) h = tail

дает:

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