Haskell Functor ley implícita

Question

Typeclassopedia dice:.

"Un argumento similar muestra también que cualquier instancia Functor que satisface la primera ley (id fmap = id) satisfará automáticamente la segunda ley, así Prácticamente, esto significa que sólo el 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 funtores?

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

Answer 1

Mientras No puedo dar una prueba, creo que lo que está diciendo es que debido a parametricity, el sistema de tipo impone la segunda ley, siempre que la primera ley sea válida. 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 es perfectamente posible definir un "mapeo" desde C a sí mismo (es decir, un par de funciones endofunctions en Obj (C) y Hom (C) respectivamente) que obedece a la primera regla, pero no obedece la segunda regla, y por lo tanto deja de constituir un funtor.

Recuerde que Functor s en Haskell son endofunctors en la categoría Hask, y ni siquiera todo lo que matemáticamente se considera un endofunctor en Hask puede expresarse en Haskell ... las limitaciones de la regla de polimorfismo paramétrico a cabo siendo capaz de especificar un functor que no se comporta de manera uniforme para todos los objetos (tipos) que mapea.

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

Dadofmap id = id, fmap (f . g) = fmap f . fmap gse deduce del teorema para libre fmap.

Esto fue publicado como un aparte en un documento hace mucho tiempo, pero se me olvida dónde.

Answer 2

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

La primera ley dice que el mapeo de la función identidad sobre cada artículo en un recipiente no tiene efecto. El segundo dice que el mapeo de una composición de dos funciones sobre cada elemento en un contenedor es el igual que la primera asignación de una función, y luego mapeo de la otra. --- Typeclassopedia

(no puedo ver por qué esta primera ley implica la segunda ley, pero no soy un experto Haskeller - es probablemente evidente cuando se sabe lo que está pasando)

Answer 3

Se

Parece que se realizó quite recently 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 ya que no he tenido el tiempo para trabajar en los detalles mí mismo, me estoy dando el beneficio de la duda aquí.)

Answer 4

Usando seq, podemos escribir una instancia que satisface la primera regla, pero no el segundo.

data Foo a = Foo a 
    deriving Show 

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

Podemos comprobar que esto satisface la primera ley:

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

Sin embargo, se rompe la segunda ley:

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

Dicho esto, por lo general ignoran tales casos patológicos.