haskell - preguntas - ¿Cuál es la relación entre profunctores y flechas?

tag de las 20 preguntas

Question

Al parecer, cada Arrow es un profunctor Strong . De hecho, ^>> y >>^ corresponden a lmap y rmap . Y first'' y second'' son lo mismo que first y second . Del mismo modo, cada ArrowChoice es también una Choice .

Lo que les falta a los profesores en comparación con las flechas es la capacidad de componerlas. Si añadimos composición, ¿obtendremos una flecha? En otras palabras, si un profesor (fuerte) también es una category , ¿ya es una flecha? Si no, ¿qué falta?

Answer 1

Lo que les falta a los profesores en comparación con las flechas es la capacidad de componerlas. Si añadimos composición, ¿obtendremos una flecha?

MONOIDES

Esta es exactamente la pregunta abordada en la sección 6 de " Nociones de computación como monoides ", que muestra un resultado de la semántica categórica para flechas (bastante densa). Las "nociones" son un gran artículo porque, aunque profundiza en la teoría de categorías, (1) no asume que el lector tiene más que un conocimiento superficial de álgebra abstracta y (2) ilustra la mayoría de las matemáticas que inducen la migraña con el código Haskell. Podemos resumir brevemente la sección 6 del documento aquí:

Digamos que tenemos

class Profunctor p where
dimap :: (contra'' -> contra) -> (co -> co'') -> p contra co -> p contra'' co''

Su codificación estándar de dividendos, negativos y positivos de los profunctores en Haskell. Ahora este tipo de datos,

data (⊗) f g contra co = forall x. (f contra x) ⊗ (g x co)

tal como se implementó en hackage.haskell.org/package/profunctors-5.2/docs/… , actúa como composición para profunctor. Podemos, por ejemplo, demostrar una instancia legítima de Profunctor :

instance (Profunctor f, Profunctor g) => Profunctor (f ⊗ g) where
dimap contra co (f ⊗ g) = (dimap contra id f) ⊗ (dimap id co g)

Agitaremos la prueba de que es legal por razones de tiempo y espacio.

DE ACUERDO. Ahora la parte divertida. Digamos que esta clase de tipos:

class Profunctor p => ProfunctorMonoid p where
e :: (a -> b) -> p a b
m :: (p ⊗ p) a b -> p a b

Esta es, con mucho más movimiento de la mano, una forma de codificar la noción de monoides profunctores en Haskell. Específicamente, se trata de un monoide en la categoría monoidal Pro , que es una estructura monoidal para la categoría de funtor [C^op x C, Set] con ⊗ como tensor y Hom como su unidad. Por lo tanto, hay una gran cantidad de dicción matemática ultraespecífica para descomprimir aquí, pero para eso solo debes leer el documento.

Entonces vemos que ProfunctorMonoid es isomorfo a Arrow ... casi.

instance ProfunctorMonoid p => Category p where
id = dimap id id
(.) pbc pab = m (pab ⊗ pbc)
instance ProfunctorMonoid p => Arrow p where
arr = e
first = undefined
instance Arrow p => Profunctor p where
lmap = (^>>)
rmap = (>>^)
instance Arrow p => ProfunctorMonoid p where
e = arr
m (pax ⊗ pxb) = pax >> pxb

Por supuesto, estamos ignorando las leyes de clase de tipos aquí, pero, como muestra el documento, funcionan de manera fantástica.

Ahora dije casi porque crucialmente no pudimos implementar first . Lo que realmente hemos hecho es demostrar un isomorfismo entre ProfunctorMonoid y flechas previas . El artículo llama Arrow sin una flecha previa . Luego pasa a mostrar que

class Profunctor p => StrongProfunctor p where
first :: p x y -> p (x, z) (y, z)
class StrongProfunctor p => StrongProfunctorMonoid p where
e :: (a -> b) -> p a b
m :: (p ⊗ p) a b -> p a b

Es necesario y suficiente para el isomorfismo deseado a la Arrow . La palabra "fuerte" proviene de una noción específica en la teoría de categorías y se describe en el artículo con una mejor redacción y un detalle más rico del que jamás podría reunir.

Así que para resumir:

• Un monoide en la categoría de profunctores es una flecha previa y viceversa. (Una versión anterior del artículo usaba el término "flechas débiles" en lugar de flechas previas, y supongo que también está bien).

• Un monoide en la categoría de profunctores fuertes es una flecha, y viceversa.

• Como la mónada es un monoide en la categoría de endofunctores, podemos pensar en la analogía SAT Functor : Profunctor :: Monad : Arrow . Este es el verdadero impulso de las nociones de computación-como-monoides.

• Las categorías de monoides y monoides son criaturas marinas suaves que aparecen en todas partes, y es una pena que algunos estudiantes pasen por la educación en informática o ingeniería de software sin que se les enseñe monoides.

• La teoría de categorías es divertida.

• Haskell es divertido.

Answer 2

La respuesta de @haoformayor (y el artículo al que se hace referencia) es una gran idea de la teoría de categorías subyacentes: ¡las categorías monoidales son bastante hermosas! - pero pensé que algún código que muestre cómo convertir una Arrow en una Strong Category y viceversa, tal como aparecen en sus respectivas bibliotecas, podría ser un apéndice útil.

import Control.Arrow
import Control.Category
import Data.Profunctor
import Data.Profunctor.Strong
import Prelude hiding (id, (.))

De una sola mano...

newtype WrapP p a b = WrapP { unwrapP :: p a b }
instance Category p => Category (WrapP p) where
id = WrapP id
WrapP p . WrapP q = WrapP (p . q)
instance (Category p, Strong p) => Arrow (WrapP p) where
first = WrapP . first'' . unwrapP
second = WrapP . second'' . unwrapP
-- NB. the first usage of id comes from (->)''s Category instance (id :: a -> a)
-- but the second uses p''s instance (id :: p a a)
arr f = WrapP $ dimap f id id

... y los demás ...

newtype WrapA p a b = WrapA { unwrapA :: p a b }
instance Arrow p => Profunctor (WrapA p) where
dimap f g p = WrapA $ arr f >>> unwrapA p >>> arr g
instance Arrow p => Strong (WrapA p) where
first'' = WrapA . first . unwrapA
second'' = WrapA . second . unwrapA