haskell - Diversión con fmap repetido

haskell do

Question

Estaba jugando con funtores, y noté algo interesante:

Trivialmente, id se puede instanciar en el tipo (a -> b) -> a -> b .

Con el funtor de lista tenemos fmap :: (a -> b) -> [a] -> [b] , que es lo mismo que el map .

En el caso del funtor ((->) r) (de Control.Monad.Instances ), fmap es la composición de la función, por lo que podemos instanciar fmap fmap fmap :: (a -> b) -> [[a]] -> [[b]] , que es equivalente a (map . map) .

Curiosamente, fmap ocho veces nos da (map . map . map) !

Entonces tenemos

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

¿Este patrón continúa? ¿Por qué por qué no? ¿Hay una fórmula para cuántos fmap s necesito para mapear una función sobre una lista anidada n veces?

Traté de escribir un script de prueba para buscar una solución al caso n = 4 , pero GHC comienza a comer demasiada memoria a alrededor de 40 fmap s.

Answer 1

No puedo explicar por qué, pero aquí está la prueba del ciclo:

Supongamos que k >= 2 y fmap^(4k) :: (a -> b) -> F1 F2 F3 a -> F1 F2 F3 b , donde Fx representa un Functor desconocido / arbitrario. fmap^n significa fmap aplicado a n-1 fmap s, no iteración n-1 fmap . El inicio de la inducción se puede verificar a mano o consultando ghci.

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

la unificación con a -> b produce a = x -> y , b = F4 x -> F4 y , entonces

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

Ahora, para fmap^(4k+2) debemos unificar F1 F2 F3 (x -> y) con (a -> b) -> F5 a -> F5 b .
Por lo tanto, F1 = (->) (a -> b) y F2 F3 (x -> y) deben unificarse con F5 a -> F5 b .
De ahí que F2 = (->) (F5 a) y F3 (x -> y) = F5 b , es decir, F5 = F3 y b = x -> y . El resultado es

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

Para fmap^(4k+3) , debemos unificar a -> (x -> y) con (m -> n) -> F6 m -> F6 n) , dando a = m -> n ,
x = F6 m e y = F6 n , entonces

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

Finalmente, debemos unificar F3 (m -> n) con (a -> b) -> F7 a -> F7 b , entonces F3 = (->) (a -> b) , m = F7 a y n = F7 b , por lo tanto

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

y el ciclo está completo. Por supuesto, el resultado proviene de consultar ghci, pero tal vez la derivación arroja algo de luz sobre cómo funciona.

Answer 2

fmap una respuesta un poco más simple: el map es una especialización de fmap y (.) También es una especialización de fmap . Entonces, por sustitución, ¡obtienes la identidad que descubriste!

Si estás interesado en ir más allá, Bartosz Milewski tiene un buen writeup que usa Yoneda Lemma para hacer explícita la razón por la que la composición de funciones es una mónada.