18 votos

Haskell Functor implícita de la ley

Typeclassopedia dice:

"Un argumento similar muestra también que cualquier Functor instancia que satisface la primera ley (fmap id = id) satisfará automáticamente a la segunda ley. Prácticamente, esto significa que sólo la primera ley necesita ser comprobado (por lo general, muy sencillo de inducción) para asegurarse de que un Functor ejemplo es válido."

Si este es el caso, ¿por qué se menciona siquiera el segundo functor de la ley?

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

16voto

pelotom Puntos 14817

Mientras que no se puede dar una prueba, yo creo que lo que esto está diciendo es que, debido a parametricity, el tipo de sistema impone la segunda ley, mientras la primera ley sostiene. La razón para especificar las reglas es que en el más general de la matemática configuración, usted podría tener una categoría C donde es perfectamente posible definir un "mapeo" de la C a la misma (es decir, un par de endofunctions en Obj(C) y Hom(C) , respectivamente) que obedece a la primera regla, pero que no obedecen a la segunda regla, y por tanto no constituyen un functor.

Recuerde que Functors en Haskell son endofunctors en la categoría de Hask, y ni siquiera todo lo que matemáticamente se considera un endofunctor en Hask puede ser expresado en Haskell... las limitaciones de polimorfismo paramétrico descartar ser capaz de especificar un functor que no se comporta de manera uniforme para todos los objetos (tipos) que se asigna.

Basado en este hilo, el consenso general parece ser que la segunda ley de la siguiente manera a partir de la primera para Haskell Functor de los casos. Edward Kmett dice,

Dado fmap id = id, fmap (f . g) = fmap f . fmap g de la siguiente manera gratuita teorema de fmap.

Este fue publicado como un aparte en un papel de mucho tiempo atrás, pero se me olvido donde.

10voto

hammar Puntos 89293

El uso de seq, podemos escribir una instancia que se cumple 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 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 el segundo de la ley:

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

Dicho esto, se suelen ignorar tales los casos patológicos.

3voto

Michael Anderson Puntos 21181

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

La primera ley dice que la asignación de la identidad de la función de cada elemento en un recipiente no tiene ningún efecto. El segundo dice que la asignación de un la composición de dos funciones de cada elemento en un contenedor mismo como primera asignación de una función y, a continuación, la asignación de los otros. --- Typeclassopedia

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

2voto

ibid Puntos 2837

Parece que se dieron cuenta hace muy poco que la ley de 2 de la siguiente manera a partir de la ley 1. Por lo tanto, cuando la documentación fue escrita originalmente, probablemente fue pensado para ser una de las necesidades primarias.

(Personalmente, no estoy convencido por el argumento, pero ya que no he tenido el tiempo para trabajar en los detalles mí mismo, voy a dar el beneficio de la duda aquí).

Iteramos.com

Iteramos es una comunidad de desarrolladores que busca expandir el conocimiento de la programación mas allá del inglés.
Tenemos una gran cantidad de contenido, y también puedes hacer tus propias preguntas o resolver las de los demás.

Powered by:

X