haskell - functors - Funtores monoidales laxos con una estructura monoidal diferente.

category theory pdf

Question

Los funtores aplicativos son bien conocidos y queridos entre los Haskellers, por su capacidad para aplicar funciones en un contexto efectivo.

En términos de categoría teórica, se puede demostrar que los métodos del Applicative :

pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b

son equivalentes a tener un Functor f con las operaciones:

unit :: f ()
(**) :: (f a, f b) -> f (a,b)

la idea es que para escribir pure simplemente reemplace () en la unit con el valor dado, y para escribir (<*>) aplaste la función y el argumento en una tupla y luego asigne una función de aplicación adecuada sobre ella.

Además, esta correspondencia convierte las leyes Applicative en leyes naturales monoidales sobre la unit y (**) , por lo que de hecho un funtor aplicativo es precisamente lo que un teórico de categorías llamaría un functor monoidal laxa (lax porque (**) es simplemente un Transformación natural y no isomorfismo).

Está bien, está bien, genial. Esto es muy conocido. Pero esa es solo una familia de funtores monoides laxos: los que respetan la estructura monoidal del producto . Un functor monoidal laxo implica dos opciones de estructura monoidal, en la fuente y el destino: esto es lo que obtiene si convierte el producto en una suma:

class PtS f where
unit :: f Void
(**) :: f a -> f b -> f (Either a b)
-- some example instances
instance PtS Maybe where
unit = Nothing
Nothing ** Nothing = Nothing
Just a ** Nothing = Just (Left a)
Nothing ** Just b = Just (Right b)
Just a ** Just b = Just (Left a) -- ick, but it does satisfy the laws
instance PtS [] where
unit = []
xs ** ys = map Left xs ++ map Right ys

Parece que convertir la suma en otras estructuras monoidales se hace menos interesante por unit :: Void -> f Void se determina de forma única, por lo que realmente tiene más de un semigrupo en curso. Pero aún:

• ¿Son otros funtores monoides laxos como los estudiados anteriormente o útiles?
• ¿Hay una buena presentación alternativa para ellos como la Applicative ?

Answer 1

Antes de que pueda hablar sobre los funtores monoidales, debe asegurarse de estar en una categoría monoidal . Sucede que Hask es una categoría monoidal de la siguiente manera:

• () como identidad
• (,) como bifunctor
• Identifique los tipos isomorfos, es decir (a,()) ≅ ((),a) ≅ a , y (a,(b,c)) ≅ ((a,b),c) .

Como observaste, también es una categoría monoidal cuando intercambias () por Void y (,) por Either .
Sin embargo, monoidal no te lleva muy lejos, lo que hace a Hask tan poderoso es que es cerrado cartesiano . Eso nos da técnicas de curry y relacionadas, sin las cuales el aplicativo sería bastante inútil.

Una categoría monoidal puede ser cartesiana cerrada si su identidad es un objeto terminal , es decir, un tipo en el que existe precisamente una flecha (por supuesto, ignoramos ⟂ aquí). Hay una función A -> () para cualquier tipo A , a saber, const () . No hay función A -> Void sin embargo. En cambio, Void es el objeto inicial : existe precisamente una flecha desde él, a saber, el absurd :: Void -> a método. Tal categoría monoidal no puede ser cartesiana cerrada entonces.
Ahora, por supuesto, puede cambiar entre inicial y terminal fácilmente girando alrededor de la dirección de la flecha. Eso siempre te coloca en la estructura dual, por lo que obtenemos una categoría cerrada cocartesiana . Pero eso significa que también necesitas voltear las flechas en tus funtores monoides. Esos son llamados funtores decisivos entonces (y generalizan comonads). Con el siempre increíble esquema de nombres de Conor,

class (Functor f) => Decisive f where
nogood :: f Void -> Void
orwell :: f (Either s t) -> Either (f s) (f t)

Answer 2

La "presentación alternativa ordenada" para Applicative se basa en las siguientes dos equivalencias

pure a = fmap (const a) unit
unit = pure ()
ff <*> fa = fmap (/(f,a) -> f a) $ ff ** fa
fa ** fb = pure (,) <*> fa <*> fb

El truco para obtener esta "presentación alternativa nítida" para Applicative es el mismo que para zipWith : reemplace los tipos y constructores explícitos en la interfaz con cosas a las que se puede pasar el tipo o el constructor para recuperar lo que era la interfaz original.

unit :: f ()

Se reemplaza con pure que podemos sustituir el tipo () y el constructor () :: () en para recuperar la unit .

pure :: a -> f a
pure () :: f ()

Y de manera similar (aunque no tan sencillo) para sustituir el tipo (a,b) y el constructor (,) :: a -> b -> (a,b) en liftA2 para recuperar ** .

liftA2 :: (a -> b -> c) -> f a -> f b -> f c
liftA2 (,) :: f a -> f b -> f (a,b)

Applicative luego obtiene el agradable operador <*> al levantar la aplicación de la función ($) :: (a -> b) -> a -> b al functor.

(<*>) :: f (a -> b) -> f a -> f b
(<*>) = liftA2 ($)

Para encontrar una "presentación alternativa nítida" para PtS necesitamos encontrar

• Algo que podemos sustituir por el tipo Void para recuperar la unit
• algo que podemos sustituir por el tipo Either ab y los constructores Left :: a -> Either ab y Right :: b -> Either ab para recuperar **

(Si te das cuenta de que ya tenemos algo en lo que se te pueden pasar los constructores Left y Right probablemente podrás averiguar con qué podemos reemplazar ** sin seguir los pasos que usé; no lo noté hasta que lo resolví)

unidad

Esto nos da de inmediato una alternativa a la unit por sumas:

empty :: f a
empty = fmap absurd unit
unit :: f Void
unit = empty

operador

Nos gustaría encontrar una alternativa a (**) . Existe una alternativa a las sumas como Either que permite que se escriban como funciones de productos. Aparece como el patrón de visitante en lenguajes de programación orientados a objetos donde no existen sumas.

data Either a b = Left a | Right b
{-# LANGUAGE RankNTypes #-}
type Sum a b = forall c. (a -> c) -> (b -> c) -> c

Es lo que obtendría si cambiara el orden de los argumentos de either de los either y los aplicara parcialmente.

either :: (a -> c) -> (b -> c) -> Either a b -> c
toSum :: Either a b -> Sum a b
toSum e = /forA forB -> either forA forB e
toEither :: Sum a b -> Either a b
toEither s = s Left Right

Podemos ver que Either ab ≅ Sum ab . Esto nos permite reescribir el tipo para (**)

(**) :: f a -> f b -> f (Either a b)
(**) :: f a -> f b -> f (Sum a b)
(**) :: f a -> f b -> f ((a -> c) -> (b -> c) -> c)

Ahora está claro lo que ** hace. Retrasa la fmap de algo a ambos argumentos y combina los resultados de esas dos asignaciones. Si introducimos un nuevo operador, <||> :: fc -> fc -> fc que simplemente asume que el fmap ya se hizo, entonces podemos ver que

fmap (/f -> f forA forB) (fa ** fb) = fmap forA fa <||> fmap forB fb

O de vuelta en términos de Either :

fa ** fb = fmap Left fa <||> fmap Right fb
fa1 <||> fa2 = fmap (either id id) $ fa1 ** fa2

Entonces podemos expresar todo lo que PtS puede expresar con la siguiente clase, y todo lo que podría implementar PtS puede implementar la siguiente clase:

class Functor f => AlmostAlternative f where
empty :: f a
(<||>) :: f a -> f a -> f a

Es casi seguro que esto es lo mismo que la clase Alternative , excepto que no requerimos que el Functor sea Applicative .

Conclusión

Es solo un Functor que es un Monoid para todos los tipos. Sería equivalente a lo siguiente:

class (Functor f, forall a. Monoid (f a)) => MonoidalFunctor f

El forall a. Monoid (fa) forall a. Monoid (fa) restricción forall a. Monoid (fa) es un pseudocódigo; No conozco una manera de expresar restricciones como esta en Haskell.

Answer 3

Mi experiencia en teoría de categorías es muy limitada, pero FWIW, tu clase de PtS me recuerda a la clase Alternative , que se parece esencialmente a esto:

class Applicative f => Alternative f where
empty :: f a
(<|>) :: f a -> f a -> f a

El único problema, por supuesto, es que Alternative es una extensión del Applicative . Sin embargo, tal vez uno pueda imaginar que se presente por separado, y la combinación con el Applicative recuerda bastante a un funtor con una estructura de anillo no conmutativa, con las dos estructuras monoides como las operaciones del anillo. También existen leyes de distribución entre el Applicative y la Alternative IIRC.