Explicación del functor aplicativo en términos categóricos - functores monoidales

Me gustaría entender Applicativeen términos de teoría de categorías.

La documentación de Applicativedice que es un functor monoidal fuerte y laxo .

Primero, la página de Wikipedia sobre los functores monoidales dice que un functor monoidal es laxo o fuerte . Entonces, me parece que una de las fuentes está equivocada o usan los términos de manera diferente. ¿Alguien puede explicar eso?

Segundo, ¿cuáles son las categorías monoidales de las cuales Applicativeson functores monoidales? Supongo que los functores son endofunctores en la categoría estándar de Haskell (objetos = tipos, morfismos = funciones), pero no tengo idea de cuál es la estructura monoidal en esta categoría.

Gracias por la ayuda.

En realidad, hay dos usos de la palabra "fuerza" en juego aquí.

• Un endofunctor fuerte sobre una categoría monoidal ( C , ⊗ , I ) es uno que viene con una transformación natural σ : A ⊗ F ( B ) → F ( A ⊗ B ) , satisfaciendo algunas condiciones de coherencia con respecto a el asociador que pasaré por alto. Esta condición a veces también se pronuncia " F tiene una fuerza".$F : C \to C$$(C, \otimes, I)$$\sigma : A \otimes F(B) \to F(A \otimes B)$$F$

• Un functor monoidal laxo es un functor entre dos categorías monoidales ( C , ⊗ , I ) y ( D , ⊕ , J ) con transformaciones naturales ϕ : F ( A ) ⊕ F ( B ) → F ( A ⊗ B ) y i : J → F ( I $F : C \to D$$(C, \otimes, I)$$(D, \oplus, J)$$\phi : F(A) \oplus F(B) \to F(A \otimes B)$$i : J \to F(I)$, nuevamente satisfaciendo una condición de coherencia con respecto a los asociadores.

• Un functor monoidal fuerte es uno en el que ϕ e i son isomorfismos naturales. Es decir, F ( A ⊗ B ) ≃ F ( A ) ⊕ F ( B ) , con ϕ y su inverso que describe el isomorfismo.$F : C \to D$$\phi$$i$$F(A \otimes B) \simeq F(A) \oplus F(B)$$\phi$

Un functor aplicativo, en el sentido de los programas Haskell, es un endofunctor monoidal laxo con una resistencia , siendo la estructura monoidal en cuestión los productos cartesianos. Por eso se obtiene el término de sonido paradójico "functor monoidal fuerte y laxo".

Por otro lado, en una categoría cerrada cartesiana, tener una fuerza es equivalente a la existencia de una transformación natural m a p : ( A ⇒ B ) → ( F ( A ) ⇒ F ( B ) ) . Es decir, tener una fuerza significa que la acción functorial se puede definir como una función de orden superior en el lenguaje de programación.$F$$\mathrm{map} : (A \Rightarrow B) \to (F(A) \Rightarrow F(B))$

Finalmente, si está interesado en la teoría de tipos de los fundores aplicativos de estilo Haskell, acabo de bloguear al respecto.

Para entender Aplicativo, como lo induce una mónada, quiero señalar la siguiente construcción:

$FA$$\mathrm{nat}(\mathrm{Hom}(A,B),FB)$