haskell - monada - ¿Cómo se relaciona el levantamiento(en un contexto de programación funcional) con la teoría de categorías?

monada programacion

Question

En cuanto a la documentación de Haskell , el levantamiento parece ser básicamente una generalización de fmap , que permite la asignación de funciones con más de un argumento.

Sin embargo, el artículo de Wikipedia sobre levantamiento ofrece una visión diferente, definiendo un "levantamiento" en términos de un morfismo en una categoría, y cómo se relaciona con los otros objetos y morfismos en la categoría (no daré los detalles aquí). Supongo que eso podría ser relevante para la situación de Haskell si estamos considerando a Cat (la categoría de categorías, lo que hace que nuestros morfismos sean funtores), pero no puedo ver cómo esta noción teórica de categoría de sustentación se relaciona con la de Haskell. Basado en el artículo vinculado, si es que lo hace.

Si los dos conceptos no están realmente relacionados, y solo tienen un nombre similar, ¿se utilizan los levantamientos (teoría de categorías) en Haskell?

Answer 1

Los ascensores, y la doble noción de extensiones, se utilizan absolutamente en Haskell, tal vez más prominentemente en la forma de extend comonádica y bind monádico. (Confusamente, extend es una elevación, no una extensión). Una comuna de extend nos permite tomar una función wa -> b y extract :: wb -> b lo largo de extract :: wb -> b para obtener un mapa wa -> wb . En el arte ASCII, dado el diagrama.

        w b
         |
         V
w a ---> b

donde se extrae la flecha vertical, extend nos da una flecha diagonal (haciendo que el diagrama se conmute):

     -> w b
    /    |
   /     V
w a ---> b

Más familiar para la mayoría de los Haskellers es la doble noción de bind ( >>= ) para una mónada m . Dada una función a -> mb y return :: a -> ma , podemos "extender" nuestra función a lo largo del return para obtener una función ma -> mb . En el arte ASCII:

a ---> m b
|
V
m a

Nos da

a ---> m b
 |  __A
 V /
m a

(¡Esa A es una punta de flecha!)

Así que sí, se podría haber llamado extend lift , y bind podría haber llamado a bind . extend . En cuanto a los lift de Haskell, ¡no tengo ni idea de por qué se llaman así!

EDIT: En realidad, creo que, de nuevo, los lift de Haskell son en realidad extensiones. Si f es aplicativo, y tenemos una función a -> b -> c , podemos componer esta función con pure :: c -> fc para obtener una función a -> b -> fc . Sin incurrir, esto es lo mismo que una función (a, b) -> fc . Ahora también podemos golpear (a, b) con pure para obtener una función (a, b) -> f (a, b) . Ahora, al fmap fst y snd , obtenemos las funciones f (a, b) -> fa y f (a, b) -> fb , que podemos combinar para obtener una función f (a, b) -> (fa, fb) . Componer con nuestro pure de antes da (a, b) -> (fa, fb) . ¡Uf! Para recapitular, tenemos el diagrama de arte ASCII

  (a, b) ---> f c
    |
    V
(f a, f b)

Ahora liftA2 nos da una función (fa, fb) -> fc , que no dibujaré porque estoy harta de hacer diagramas terribles. Pero el punto es que el diagrama conmuta, por lo que liftA2 realidad nos da una extensión de la flecha horizontal a lo largo de la vertical.