opciones - programa en haskell
La teoría de la mónada y Haskell (9)
La mayoría de los tutoriales parecen dar muchos ejemplos de mónadas (IO, estado, lista, etc.) y luego esperan que el lector sea capaz de abstraer el principio general y luego mencionan la teoría de categorías. No tiendo a aprender muy bien tratando de generalizar a partir de ejemplos y me gustaría entender desde un punto de vista teórico por qué este patrón es tan importante.
A juzgar por este hilo: ¿Alguien puede explicar las Mónadas? este es un problema común, y he intentado ver la mayoría de los tutoriales sugeridos (excepto los videos de Brian Beck que no se reproducirán en mi máquina Linux):
¿Alguien sabe de un tutorial que parte de la teoría de categorías y explica IO, estado, enumera mónadas en esos términos? el siguiente es mi intento fallido de hacerlo:
Según entiendo, una mónada consiste en un triple: un endofunctor y dos transformaciones naturales.
El funtor usualmente se muestra con el tipo: (a -> b) -> (ma -> mb) Incluí el segundo paréntesis solo para enfatizar la simetría.
Pero, este es un endofunctor, ¿entonces el dominio y el codominio no deberían ser los mismos así ?:
(a -> b) -> (a -> b)
Creo que la respuesta es que tanto el dominio como el codomain tienen un tipo de:
(a -> b) | (ma -> mb) | (mma -> mmb) y así sucesivamente ...
Pero no estoy muy seguro de si eso funciona o encaja con la definición del funtor dado?
Cuando pasamos a la transformación natural, empeora. Si entiendo correctamente una transformación natural es un functor de segundo orden (con ciertas reglas) que es un funtor de un funtor a otro. Entonces, como hemos definido el functor arriba, el tipo general de las transformaciones naturales sería: ((a -> b) -> (ma -> mb)) -> ((a -> b) -> (ma -> mb )
Pero las transformaciones naturales reales que estamos utilizando tienen tipo:
a -> ma
ma -> (a -> mb) -> mb
¿Estos subconjuntos de la forma general están arriba? y ¿por qué son transformaciones naturales?
Martín
Si bien las mónadas originalmente provenían de la teoría de categorías, esto no significa que la teoría de categorías sea el único contexto abstracto en el que puede verlas. Un punto de vista diferente viene dado por la semántica operacional . Para una introducción, eche un vistazo a mi tutorial Operational Monad .
Un descargo de responsabilidad rápido: me siento un poco inestable en cuanto a la teoría de categorías en general, aunque me da la impresión de que al menos está familiarizado con ella. Con suerte, no haré demasiado ruido de esto ...
¿Alguien sabe de un tutorial que parte de la teoría de categorías y explica IO, estado, enumera mónadas en esos términos?
Antes que nada, ignora IO por ahora, está lleno de magia oscura. Funciona como un modelo de cálculos imperativos por las mismas razones por las que el State trabaja para modelar cómputos con estado, pero a diferencia del último IO es una caja negra sin forma de deducir la estructura monádica desde el exterior.
El funtor usualmente se muestra con el tipo: (a -> b) -> (ma -> mb) Incluí el segundo paréntesis solo para enfatizar la simetría.
Pero, este es un endofunctor, ¿entonces el dominio y el codominio no deberían ser los mismos así ?:
Sospecho que está malinterpretando cómo las variables de tipo en Haskell se relacionan con los conceptos de la teoría de categorías.
En primer lugar, sí, eso especifica un endofunctor, en la categoría de tipos Haskell. Sin embargo, a variable de tipo como a no es nada en esta categoría; es una variable que (implícitamente) se cuantifica universalmente sobre todos los objetos en la categoría. Por lo tanto, el tipo (a -> b) -> (a -> b) describe solo endofunctors que asignan cada objeto a sí mismo .
Los constructores de tipo describen una función de inyección en los objetos, donde los elementos del codominio del constructor no pueden describirse por ningún medio excepto como una aplicación del constructor de tipo. Incluso si dos constructores de tipo producen resultados isomorfos, los tipos resultantes siguen siendo distintos. Tenga en cuenta que los constructores de tipos no son, en el caso general, funtores.
La variable de tipo m en la firma del functor, entonces, representa un constructor de tipo de un argumento. Fuera de contexto, esto normalmente se leería como cuantificación universal, pero eso es incorrecto en este caso, ya que no puede existir tal función. Por el contrario, la definición de la clase de tipo vincula m y permite la definición de tales funciones para constructores de tipos específicos .
La función resultante, entonces, dice que para cualquier constructor de tipo m que tenga definido fmap , para dos objetos a y b y un morfismo entre ellos, podemos encontrar un morfismo entre los tipos dados aplicando m a a y b .
Tenga en cuenta que, si bien lo anterior, por supuesto, define un endofunctor en Hask , ni siquiera es remotamente lo suficientemente general como para describir todos los endofunctors.
Pero las transformaciones naturales reales que estamos utilizando tienen tipo:
a -> ma
ma -> (a -> mb) -> mb
¿Estos subconjuntos de la forma general están arriba? y ¿por qué son transformaciones naturales?
Bueno, no, no lo son. Una transformación natural es más o menos una función (no un functor) entre funtores. Las dos transformaciones naturales que especifican una mónada M se ven como I -> M donde I es el funtor de identidad, y M ∘ M -> M donde ∘ es la composición del funtor. En Haskell, no tenemos una buena manera de trabajar directamente con un verdadero functor de identidad o con la composición de un funtor. En su lugar, descartamos el functor de identidad para obtener just (Functor m) => a -> ma para el primero y escribir la aplicación de constructor de tipo anidado como (Functor m) => m (ma) -> ma para el segundo.
El primero de estos es obviamente el return ; el segundo es una función llamada join , que no es parte de la clase de tipo. Sin embargo, join se puede escribir en términos de (>>=) , y este último es más útil en la programación diaria.
En cuanto a mónadas específicas, si desea una descripción más matemática, aquí hay un boceto rápido de un ejemplo:
Para algún tipo fijo S, considere dos funtores F y G donde F (x) = (S, x) y G (x) = S -> x (Debería ser obvio que estos son funtores válidos).
Estos funtores también son adjuntos; Considere las transformaciones naturales unit :: x -> G (F x) y counit :: F (G x) -> x . Expandir las definiciones nos da unit :: x -> (S -> (S, x)) y counit :: (S, S -> x) -> x . Los tipos sugieren aplicación de función no ejecutada y construcción de tuplas; siéntete libre de verificar que esos funcionen como se espera.
Una adjunción da lugar a una mónada por composición de los funtores, por lo que tomando G ∘ F y expandiendo la definición, obtenemos G (F x) = S -> (S, x), que es la definición de la mónada de State . La unit para la adjunción es, por supuesto, de return ; y deberías poder usar counit para definir join .
La mejor manera de observar las mónadas y los efectos computacionales es comenzar con el punto en el que Haskell obtuvo la noción de mónadas para los efectos computacionales, y luego observar a Haskell después de que usted lo comprenda. Ver este documento en particular: Nociones de Computación y Mónadas , por E. Moggi.
Véase también el documento anterior de Moggi que muestra cómo funcionan las mónadas para el cálculo lambda solo: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.2787
El hecho de que las mónadas capturen la sustitución, entre otras cosas (http://blog.sigfpe.com/2009/12/where-do-monads-come-from.html), y la sustitución es clave para el cálculo lambda, debería dar una buena pista de por qué tienen tanto poder expresivo.
Una forma de ver IO es considerarlo como un extraño tipo de mónada de estado. Recuerde que la mónada estatal se ve así:
data State s a = State (s -> (s, a))
donde el argumento "s" es el tipo de datos que desea enhebrar a través del cálculo. Además, esta versión de "Estado" no tiene acciones de "obtener" y "poner" y no exportamos el constructor.
Ahora imagina un tipo
data RealWorld = RealWorld ......
Esto no tiene una definición real, pero teóricamente un valor de tipo RealWorld mantiene el estado de todo el universo fuera de la computadora. Por supuesto, nunca podemos tener un valor de tipo RealWorld, pero puedes imaginar algo como:
getChar :: RealWorld -> (RealWorld, Char)
En otras palabras, la función "getChar" toma un estado del universo antes de que se presione el botón del teclado, y devuelve la tecla presionada más el estado del universo después de presionar la tecla. Por supuesto, el problema es que el estado anterior del mundo todavía está disponible para ser referenciado, lo que no puede suceder en la realidad.
Pero ahora escribimos esto:
tipo IO = Estado RealWorld
getChar :: IO Char
En teoría, todo lo que hemos hecho es ajustar la versión anterior de "getChar" como una acción estatal. Pero al hacer esto ya no podemos acceder a los valores de "RealWorld" porque están envueltos dentro de la mónada de estado.
Entonces, cuando un programa Haskell quiere cambiar una bombilla, toma la bombilla y aplica una función de "rotación" al valor de RealWorld dentro de IO.
En términos generales, Haskell hace su teoría de categorías en una sola categoría, cuyos objetos son tipos Haskell y cuyas flechas son funciones entre estos tipos. Definitivamente no es un lenguaje de propósito general para modelar la teoría de categorías.
Un functor (matemático) es una operación que convierte las cosas en una categoría en cosas en otra categoría, posiblemente completamente diferente. Un endofunctor es entonces un functor que tiene las mismas categorías de origen y destino. En Haskell, un functor es una operación que convierte las cosas en la categoría de tipos Haskell en otras cosas también en la categoría de tipos Haskell, por lo que siempre es un endofunctor.
[Si está siguiendo la literatura matemática, técnicamente, la operación ''(a-> b) -> (ma -> mb)'' es solo la parte de la flecha del endofunctor m, y ''m'' es la parte del objeto ]
Cuando Haskellers habla de trabajar "en una mónada", realmente quieren decir trabajar en la categoría de Kleisli de la mónada. La categoría Kleisli de una mónada es una bestia completamente confusa al principio, y normalmente necesita al menos dos colores de tinta para dar una buena explicación, así que tome el siguiente intento por lo que es y revise algunas referencias (desafortunadamente Wikipedia es inútil aquí para todo menos las definiciones directas).
Supongamos que tiene una mónada ''m'' en la categoría C de tipos Haskell. Su categoría Kleisli Kl (m) tiene los mismos objetos que C, es decir, tipos Haskell, pero una flecha a ~ (f) ~> b en Kl (m) es una flecha a - (f) -> mb en C. (I He usado una línea ondulada en mi flecha Kleisli para distinguirlos a los dos). Para reiterar: los objetos y flechas del Kl (C) también son objetos y flechas de C, pero las flechas apuntan a diferentes objetos en Kl (C) que en C. Si esto no te parece impar, léelo de nuevo más ¡cuidadosamente!
Concretamente, considere la posibilidad de mónada. Su categoría Kleisli es solo la colección de tipos Haskell, y sus flechas a ~ (f) ~> b son funciones a - (f) -> Quizás b. O considere la mónada (Estado) cuyas flechas a ~ (f) ~> b son funciones a - (f) -> (Estado sb) == a - (f) -> (s -> (s, b)) . En cualquier caso, siempre está escribiendo una flecha ondulada como una abreviatura para hacer algo al tipo del codominio de sus funciones.
[Tenga en cuenta que State no es una mónada, porque el tipo de estado es * -> * -> *, por lo que debe proporcionar uno de los parámetros de tipo para convertirlo en una mónada matemática.]
Hasta ahora todo bien, con suerte, pero supongamos que quiere componer las flechas a ~ (f) ~> b y b ~ (g) ~> c. Estas son realmente funciones Haskell a - (f) -> mb yb - (g) -> mc que no se pueden componer porque los tipos no coinciden. La solución matemática es usar la transformación natural de "multiplicación" u: mm-> m de la mónada de la siguiente manera: a ~ (f) ~> b ~ (g) ~> c == a - (f) -> mb - (mg) -> mmc - (u_c) -> mc para obtener una flecha a-> mc que es una flecha Kleisli a ~ (f; g) ~> c según se requiera.
Quizás un ejemplo concreto ayude aquí. En la mónada Quiz, no puedes componer funciones f: a -> Tal vez b y g: b -> Quizás c directamente, pero levantando g para
Maybe_g :: Maybe b -> Maybe (Maybe c)
Maybe_g Nothing = Nothing
Maybe_g (Just a) = Just (g a)
y usando lo ''obvio''
u :: Maybe (Maybe c) -> Maybe c
u Nothing = Nothing
u (Just Nothing) = Nothing
u (Just (Just c)) = Just c
puedes formar la composición u . Maybe_g . f u . Maybe_g . f u . Maybe_g . f cual es la función a -> Quizás c que querías.
En la mónada (estatal), es similar pero más desordenado: dadas dos funciones monádicas a ~ (f) ~> b y b ~ (g) ~> c que son realmente a - (f) -> (s -> (s) , b)) yb - (g) -> (s -> (s, c)) debajo del capó, usted los compone levantando g en
State_s_g :: (s->(s,b)) -> (s->(s,(s->(s,c))))
State_s_g p s1 = let (s2, b) = p s1 in (s2, g b)
entonces aplicas la transformación natural de ''multiplicación'', que es
u :: (s->(s,(s->(s,c)))) -> (s->(s,c))
u p1 s1 = let (s2, p2) = p1 s1 in p2 s2
que (tipo de) conecta el estado final de f en el estado inicial de g .
En Haskell, esto resulta ser una forma poco natural de trabajar, así que en su lugar está la función (>>=) que básicamente hace lo mismo que tú, pero de una forma que facilita su implementación y uso. Esto es importante: (>>=) no es la transformación natural ''u''. Puede definir cada uno en términos del otro, por lo que son equivalentes, pero no son lo mismo. La versión Haskell de ''u'' está escrita join .
La otra cosa que falta en esta definición de categorías Kleisli es la identidad en cada objeto: a ~ (1_a) ~> a que es realmente a - (n_a) -> ma donde n es la transformación natural de la ''unidad''. Esto se escribe en Haskell, y no parece causar tanta confusión.
Aprendí teoría de categorías antes de llegar a Haskell, y también tuve dificultades con la falta de correspondencia entre lo que los matemáticos llaman una mónada y cómo se ven en Haskell. ¡No es más fácil desde la otra dirección!
Para mí, hasta ahora, la explicación que más se aproxima para unir las mónadas en la teoría de categorías y las mónadas en Haskell es que las mónadas son un monid cuyos objetos tienen el tipo a-> m b. Veo que estos objetos están muy cerca de un endofunctor y, por lo tanto, la composición de tales funciones está relacionada con una secuencia imperativa de enunciados de programa. También las funciones que devuelven funciones IO son válidas en código funcional puro hasta que se llame a la función interna desde el exterior.
Este elemento id es ''a -> ma'' que encaja muy bien, pero el elemento de multiplicación es la composición de la función, que debería ser:
(> =>) :: Monad m => (a -> mb) -> (b -> mc) -> (a -> mc)
Esta no es exactamente la composición de la función, pero lo suficientemente cerca (creo que para obtener una verdadera composición de funciones necesitamos una función complementaria que devuelva mb a a, entonces obtenemos composición de funciones si las aplicamos en pares?), No estoy seguro cómo pasar de eso a esto:
(>> =) :: Monad m => ma -> (a -> mb) -> mb
Tengo la sensación de que pude haber visto una explicación de esto en todas las cosas que leí, sin comprender su significado la primera vez, así que haré algunas relecturas para tratar de (re) encontrar una explicación de esto. .
Otra cosa que me gustaría hacer es vincular todas las diferentes explicaciones de la teoría de categorías: endofunctor + 2 transformaciones naturales, categoría Kleisli, un monoide cuyos objetos son monoides, etc. Para mí, lo que parece vincular todas estas explicaciones es que son de dos niveles. Es decir, normalmente tratamos los objetos de categoría como cuadros negros donde implicamos sus propiedades a partir de sus interacciones externas, pero aquí parece ser necesario pasar un nivel dentro de los objetos para ver qué está sucediendo. Podemos explicar las mónadas sin esto, pero solo si aceptamos construcciones aparentemente arbitrarias.
Martín
Esta página hace exactamente eso. Creo que tu principal confusión es que la clase realmente no hace que el tipo sea un funtor, sino que define un funtor de la categoría de tipos Haskell en la categoría de ese tipo.
Siguiendo la notación del enlace, suponiendo que F es un Funktor Haskell, significa que hay un funtor de la categoría de Hask a la categoría de F.
No estoy seguro de entender cuál fue la pregunta, pero sí, tienes razón, la mónada en Haskell se define como un triple:
m :: * -> * -- this is endofunctor from haskell types to haskell types!
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
pero la definición común de la teoría de categorías es otra triple:
m :: * -> *
return :: a -> m a
join :: m (m a) -> m a
Es un poco confuso pero no es tan difícil mostrar que estas dos definiciones son iguales. Para hacer eso necesitamos definir join en términos de (>>=) (y viceversa). Primer paso:
join :: m (m a) -> m a
join x = ?
Esto nos da x :: m (ma) .
Todo lo que podemos hacer con algo que tiene el tipo m _ es aplicarlo (>> =) a él:
(x >>=) :: (m a -> m b) -> m b
Ahora necesitamos algo como un segundo argumento para (>> =), y también, del tipo de unión tenemos restricción (x >>= y) :: ma .
Entonces, aquí tendrá el tipo y :: ma -> ma e id :: a -> a ajusta muy bien:
join x = x >>= id
La otra manera
(>>=) :: ma -> (a -> mb) -> m b
(>>=) x y = ?
Donde x :: ma e y :: a -> mb . Para obtener mb de y , necesitamos algo de tipo a .
Desafortunadamente, no podemos extraer a de ma . Pero podemos sustituirlo por otra cosa (recuerde, la mónada también es un functor):
fmap :: (a -> b) -> m a -> m b
fmap y x :: m (m b)
Y se ajusta perfectamente como argumento para join : (>>=) xy = join (fmap yx) .
Vea esta pregunta: ¿encadenar operaciones es lo único que resuelve la clase de mónadas?
En él, explico mi visión de que debemos diferenciar entre la clase Monad y los tipos individuales que resuelven problemas individuales. La clase Monad, por sí sola, solo resuelve el importante problema de "encadenar operaciones con elección" y hace que esta solución esté disponible para los tipos que son instancia de ella (por medio de "herencia").
Por otro lado, si un tipo dado que resuelve un problema dado enfrenta el problema de "encadenar operaciones con elección", entonces, se debe convertir en una instancia (heredar) de la clase Mónada.
El hecho es que los problemas no se resuelven simplemente por ser una Mónada. Sería como decir que las "ruedas" resuelven muchos problemas, pero en realidad las "ruedas" solo resuelven un problema, y las cosas con ruedas resuelven muchos problemas diferentes.