math - Ley implícita de Haskell Functor

applicative functor

Question

Typeclassopedia dice:

"Un argumento similar también muestra que cualquier instancia de Functor que satisfaga la primera ley (fmap id = id) también satisfará automáticamente la segunda ley. Prácticamente, esto significa que solo se debe verificar la primera ley (generalmente mediante una inducción muy directa) para garantizar que una instancia de Functor sea válida ".

Si este es el caso, ¿por qué mencionamos siquiera la segunda ley de fideicomiso?

Law 1: fmap id = id
Law 2: fmap (g . h) = (fmap g) . (fmap h)

Answer 1

Parece que recientemente se realizó que la ley 2 se sigue de la ley 1. Por lo tanto, cuando la documentación se escribió originalmente, probablemente se pensó que era un requisito independiente.

(Personalmente, no estoy convencido por el argumento, pero dado que no he tenido el tiempo de resolver los detalles yo mismo, le doy aquí el beneficio de la duda).

Answer 2

Si bien no puedo dar una prueba, creo que lo que esto está diciendo es que debido a la parametricidad , el sistema de tipo impone la segunda ley siempre que la primera ley se cumpla. La razón para especificar ambas reglas es que en la configuración matemática más general, puede tener alguna categoría C donde sea perfectamente posible definir un "mapeo" desde C a sí mismo (es decir, un par de funciones finales en Obj ( C ) y Hom ( C ) respectivamente) que obedece a la primera regla pero no obedece la segunda regla, y por lo tanto no puede constituir un funtor.

Recuerda que los Functor en Haskell son endofuntores en la categoría Hask , y ni siquiera todo lo que matemáticamente podría considerarse un endofunctor en Hask se puede expresar en Haskell ... las restricciones del polimorfismo paramétrico descartan poder especificar un functor que no lo haga comportarse uniformemente para todos los objetos (tipos) que mapea.

Basado en este hilo , el consenso general parece ser que la segunda ley se sigue de la primera para las instancias de Haskell Functor . Edward Kmett dice ,

Dado fmap id = id , fmap (f . g) = fmap f . fmap g fmap (f . g) = fmap f . fmap g sigue del teorema libre para fmap.

Esto fue publicado como un aparte en un periódico hace mucho tiempo, pero olvido dónde.

Answer 3

Usando seq , podemos escribir una instancia que satisfaga la primera regla pero no la segunda.

data Foo a = Foo a
    deriving Show

instance Functor Foo where
    fmap f (Foo x) = f `seq` Foo (f x)

Podemos verificar que esto satisface la primera ley:

fmap id (Foo x)
= id `seq` Foo (id x)
= Foo (id x)
= Foo x

Sin embargo, rompe la segunda ley:

> fmap (const 42 . undefined) $ Foo 3
Foo 42
> fmap (const 42) . fmap undefined $ Foo 3
*** Exception: Prelude.undefined

Dicho esto, solemos ignorar tales casos patológicos.

Answer 4

Yo diría que la segunda ley no se menciona por razones de validez, sino más bien como una propiedad importante:

La primera ley dice que mapear la función de identidad sobre cada elemento en un contenedor no tiene ningún efecto. El segundo dice que mapear una composición de dos funciones sobre cada elemento en un contenedor es lo mismo que mapear primero una función y luego mapear la otra. --- Typeclassopedia

(No puedo ver por qué esta primera ley implica la segunda ley, pero no soy un Haskeller habilidoso, es probable que sea obvio cuando sabes lo que está pasando)