haskell - morfismo - ¿Qué es la definición de Funcator aplicativo de la teoría de categorías POV?

morfismo matematico (2)

La clave para comprender los funtores aplicativos es averiguar qué estructura conservan.

Los funtores regulares conservan la estructura categórica básica: mapean objetos y morfismos entre categorías, y preservan las leyes de la categoría (asociatividad e identidad).

Pero una categoría puede tener más estructura. Por ejemplo, puede permitir la definición de asignaciones que son como morfismos pero que toman múltiples argumentos. Dichas asignaciones se definen mediante curry: por ejemplo, una función de dos argumentos se define como una función de un argumento que devuelve otra función. Esto es posible si puede definir un objeto que represente un tipo de función. En general, este objeto se llama exponencial (en Haskell, es solo el tipo b->c ). Entonces podemos tener morfismos de un objeto a un exponencial y llamarlo un morfismo de dos argumentos.

La definición tradicional de un funtor aplicativo en Haskell se basa en la idea de mapear funciones de múltiples argumentos. Pero hay una definición equivalente que divide la función multi-argumento a lo largo de un límite diferente. Puede ver dicha función como una asignación de un producto (un par, en Haskell) a otro tipo (aquí, c ).

a -> (b -> c) ~ (a, b) -> c

Eso nos permite ver a los funtores aplicativos como funtores que preservan el producto. Pero un producto es solo un ejemplo de lo que se llama una estructura monoidal.

En general, una categoría monoidal es una categoría equipada con un producto tensorial y un objeto unitario. En Haskell, este podría ser, por ejemplo, el producto cartesiano (un par) y el tipo de unidad () . Tenga en cuenta, sin embargo, que las leyes monoidales (asociatividad y leyes de unidad) son válidas solo hasta un isomorfismo. Por ejemplo:

(a, ()) ~ a

Un funtor aplicativo podría entonces definirse como un funtor que conserva la estructura monoidal. En particular, debe preservar la unidad y el producto. No debería importar si hacemos la "multiplicación" antes o después de aplicar el functor. Los resultados deben ser isomorfos.

Sin embargo, realmente no necesitamos un funtor monoidal en toda regla. Todo lo que necesitamos son dos morfismos (a diferencia de los isomorfismos): uno para la multiplicación y otro para la unidad. Un funtor de este tipo que conserva a medias la estructura monoidal se denomina functor monoidal laxa . De ahí la definición alternativa:

class Functor f => Monoidal f where unit :: f () (**) :: f a -> f b -> f (a, b)

Es fácil demostrar que Monoidal es equivalente a Applicative . Por ejemplo, podemos obtener pure de la unit y viceversa:

pure x = fmap (const x) unit unit = pure ()

Las leyes aplicativas se derivan simplemente de la preservación de las leyes de monoides (leyes de asociatividad y unidad).

En la teoría de categorías, la preservación de la estructura monoidal está relacionada con la fuerza tensorial , por lo que un functor aplicativo también se conoce como un functor monoidal laxa fuerte . Sin embargo, en Hask , cada funtor tiene una fuerza canónica con respecto al producto, por lo que esta propiedad no agrega nada a la definición.

Ahora, si está familiarizado con la definición de una mónada como monoide en la categoría de endofunctores, podría interesarle saber que los aplicativos son, de manera similar, los monoides en la categoría de endofunctores donde el producto tensorial es la convolución del Día. Pero eso es mucho más difícil de explicar.

Pude mapear la definición de Functor desde la teoría de categorías a la definición de Haskell de la siguiente manera: como los objetos de Hask son tipos, el functor F

asigna cada tipo a de Hask al nuevo tipo F a al decir, más o menos, antes de "F".
asigna cada morfismo a -> b de Hask al nuevo morfismo F a -> F b usando fmap :: (a -> b) -> (fa -> fb) .

Hasta ahora tan bueno. Ahora llego al Applicative y no puedo encontrar ninguna mención de tal concepto en los libros de texto. Al observar lo que agrega a Functor , ap :: f (a -> b) -> fa -> fb , traté de encontrar mi propia definición.

Primero, noté que dado que (->) también es un tipo, los morfismos de Hask son objetos de este. A la luz de esto, hice una sugerencia de que el funtor aplicativo es un funtor que también puede mapear los objetos "flecha" de la categoría de origen en los morfismos del destino.

¿Es esta una intuición correcta? ¿Puedes dar una definición más formal y rigurosa?

Tienes razón, el Applicative traduce de manera menos directa que Functor o Monad . Pero en esencia, es la clase de los en.wikipedia.org/wiki/Monoidal_functor :

class Functor f => Monoidal f where pureUnit :: f () fzip :: f a -> f b -> f (a,b)

A partir de eso puedes definir - dentro de Hask -

pure x = fmap (const x) pureUnit

fs <*> xs = fmap (uncurry ($)) $ fzip fs xs