Удовольствие с повторным fmap

Я играл с функторами, и я заметил что-то интересное:

Тривиально, id может быть создан в типе (a -> b) -> a -> b.

С функтором списка имеем fmap :: (a -> b) -> [a] -> [b], что совпадает с map.

В случае функтора ((->) r) (из Control.Monad.Instances), fmap является композицией функций, поэтому мы можем создать экземпляр fmap fmap fmap :: (a -> b) -> [[a]] -> [[b]], что эквивалентно (map . map).

Интересно, что fmap восемь раз дает нам (map . map . map)!

Итак, мы имеем

0: id = id
1: fmap = map
3: fmap fmap fmap = (map . map)
8: fmap fmap fmap fmap fmap fmap fmap fmap = (map . map . map)

Продолжается ли этот шаблон? Почему, почему нет? Есть ли формула для количества fmap Мне нужно отобразить функцию по n-разному вложенному списку?

Я попробовал написать тест script для поиска решения для случая n = 4, но GHC начинает потреблять слишком много памяти около 40 fmap s.

Ответы

Ответ 1

Я не могу объяснить, почему, но здесь доказательство цикла:

Предположим k >= 2 и fmap^(4k) :: (a -> b) -> F1 F2 F3 a -> F1 F2 F3 b, где Fx обозначает неизвестный/произвольный Functor. fmap^n означает fmap, примененный к n-1 fmap s, а не n -кратной итерации. Начало индукции можно проверить вручную или запросить ghci.

fmap^(4k+1) = fmap^(4k) fmap
fmap :: (x -> y) -> F4 x -> F4 y

объединение с a → b дает a = x -> y, b = F4 x -> F4 y, поэтому

fmap^(4k+1) :: F1 F2 F3 (x -> y) -> F1 F2 F3 (F4 x -> F4 y)

Теперь, для fmap^(4k+2), мы должны объединить F1 F2 F3 (x -> y) с (a -> b) -> F5 a -> F5 b.
Таким образом, F1 = (->) (a -> b) и F2 F3 (x -> y) должны быть унифицированы с помощью F5 a -> F5 b.
Следовательно, F2 = (->) (F5 a) и F3 (x -> y) = F5 b, т.е. F5 = F3 и b = x -> y. Результатом является

fmap^(4k+2) :: F1 F2 F3 (F4 x -> F4 y)
             = (a -> (x -> y)) -> F3 a -> F3 (F4 x -> F4 y)

Для fmap^(4k+3) мы должны унифицировать a -> (x -> y) с помощью (m -> n) -> F6 m -> F6 n), давая a = m -> n,
x = F6 m и y = F6 n, поэтому

fmap^(4k+3) :: F3 a -> F3 (F4 x -> F4 y)
             = F3 (m -> n) -> F3 (F4 F6 m -> F4 F6 n)

Наконец, мы должны объединить F3 (m -> n) с (a -> b) -> F7 a -> F7 b, поэтому F3 = (->) (a -> b), m = F7 a и n = F7 b, поэтому

fmap^(4k+4) :: F3 (F4 F6 m -> F4 F6 n)
             = (a -> b) -> (F4 F6 F7 a -> F4 F6 F7 b)

и цикл завершен. Конечно, результат следует из запроса ghci, но, возможно, вывод проливает свет на то, как он работает.

Ответ 2

Я дам немного более простой ответ: map является специализацией fmap, а (.) также является специализацией fmap. Таким образом, путем замены вы получаете идентификационную информацию, которую вы обнаружили!

Если вы заинтересованы в дальнейшем, Bartosz Milewski имеет приятный writeup, в котором используется лемма Yoneda, чтобы четко указать, почему композиция функции монада.