haskell - category theory for programmers

¿Cuáles son exactamente las categorías que están asignando los Functors aplicativos?

Question

He estado leyendo sobre Functive Functors y tengo dificultades para conciliar una discordancia en las respectivas terminologías de la teoría de categorías y la programación funcional .

Aunque he revisado varios blogs, los recursos más completos que he estado usando para esta investigación son:

• McBride & Paterson - Programación aplicativa con efectos (PDF)
• Gibbons y Oliveira - La esencia del patrón iterador (PDF)
• Tomas Petricek - Escribiendo expresiones idiomáticas en LINQ

En la teoría de categorías, un functor es un morfismo de una categoría de source a una categoría target (en una categoría de categorías). La "categoría de categorías" tiene una colección de objetos que contiene las categorías de origen y destino y una colección de functores que contiene: el functor de identidad de la categoría de origen; functor de identidad de la categoría objetivo; y, el funtor que conecta la fuente con el objetivo (si la categoría de origen es la misma que la categoría de destino y el funtor en cuestión es la identidad, entonces solo debe haber un funtor).

En la programación funcional, los funtores aplicativos se describen como un par de operaciones:

• pure : a -> fa
• <*> : f ( a -> b) -> fa -> fb .

Aquí está mi pregunta

¿Qué interpretación aclara la correspondencia entre la definición de programación funcional de un funtor aplicativo y la definición teórica de categoría de un funtor?

Más específicamente, a qué partes de la tupla (pure,<*>) corresponden a:

1. la categoría de fuente
2. la categoría de destino
3. la categoría donde vive el functor
4. El efecto de preservación de la estructura del functor en los objetos de la categoría de fuente.
5. El efecto conservador de la estructura del functor sobre los morfismos de la categoría de fuente.

Notas: Reconozco que esta puede ser una metáfora incompleta, y puede que no haya una correspondencia uno a uno para cada uno de los conceptos que mencioné. Me he abstenido deliberadamente de compartir mi especulación acerca de las correspondencias aparentes aquí para mantener mi pregunta simple y evitar confundir más los problemas.

Answer 1

La forma en que formuló su pregunta sugiere que está buscando una categoría de categorías, cuyos morfismos pueden entenderse como funtores de Haskell. Eso sería algo así. La categoría tiene un objeto que es *, que representa la categoría de los tipos de haskel. Dado que solo hay un objeto, solo tiene que haber un conjunto de morfismos, que son los constructores de tipo (de tipo * -> *). No todo constructor de tipos es un functor, pero cada funtor es un constructor de tipos. Entonces, en este sentido, se puede entender como un morfismo de * a *.

El punto de los tipos es, por supuesto, realizar un seguimiento del número de argumentos de un constructor de tipos. Entender esto como una categoría es algo artificial, ya que solo tiene un objeto.

Además, no existe un morfismo de identidad real para el objeto * . Se podría pensar en Identity :: * -> * , pero no es una identidad en sentido estricto (aunque se trata de un isomorfismo natural, ya que tienes Identity :: forall a . a -> Identity a y runIdentity :: forall a . Identity a -> a ). Lo mismo ocurre con la composición: siempre se debe utilizar un isomorfismo explícito para tratar con los funtores compuestos ( Compose / getCompose ).

Answer 2

Parafraseando esta respuesta : los funtores aplicativos son funtores para los cuales también existe una transformación natural que preserva la estructura monoidal de sus categorías de origen / objetivo. En el caso de los endofunctores Applicative de Haskell (debido a que sus categorías de origen y objetivo es Hask), la estructura monoidal es el producto cartesiano. Así que para un funtor Applicative hay transformaciones naturales φ: (fa, fb) -> f (a, b) y ι: () -> f () . Así podríamos definir Applicative como

class Functor f => Applicative'' f where
φ :: (f a, f b) -> f (a, b)
ι :: f () -- it could be /() -> f (),
-- but /() -> ... is redundant

Esta definición es equivalente a la estándar. Podemos expresar

φ = uncurry (liftA2 (,))
= /(x, y) -> (,) <$> x <*> y
ι = pure ()

y por el contrario

pure x = fmap (/() -> x) ι
f <*> x = fmap (uncurry ($)) (φ (f, x))

Tan pure y <*> es una forma alternativa de definir esta transformación natural.

Answer 3

Probablemente sea más sencillo ver primero la clase Functor (que es una superclase de Applicative ). Applicative corresponde a un "funtor monoidal lax", como lo señala el primer artículo que vinculó. La definición de Functor es:

class Functor f where
fmap :: (a -> b) -> f a -> f b

Una instancia de Functor es un constructor de tipo (de tipo * -> * ). Un ejemplo es Maybe .

La categoría de la que estamos hablando es la categoría "Hask" que tiene tipos Haskell como objetos y funciones (monomórficas) Haskell como morfismos. Cada instancia de Functor (y Applicative , Monad , etc.) es un endofunctor en esta categoría, es decir, un funtor de la categoría a sí mismo.

Los dos mapas del functor - Funciones de Haskell a Tipos de Haskell y Funciones de Haskell - Funciones de Haskell - son el constructor de tipo f y la función fmap .

Por ejemplo, Int y Maybe Int son objetos en Hask; Maybe mapas del primero al segundo. Si chr :: Int -> Char , entonces fmap mapea a fmap chr :: Maybe Int -> Maybe Char . Las leyes del Functor corresponden a las leyes del funtor categórico.

En el caso de Applicative , Functor es una superclase, por lo que se aplica todo lo que acabo de decir. En este caso particular, puede implementar fmap utilizando pure y <*> - liftA fx = pure f <*> x - así que las dos partes del functor que estaba buscando son f y liftA . (Pero tenga en cuenta que otras formulaciones de Applicative no le permiten hacer eso, en general confiaría en la superclase de Functor ).

No estoy muy seguro de qué quiere decir aquí con "la categoría en la que vive el functor".