¿Por qué los efectos secundarios se modelan como mónadas en Haskell?

¿Alguien podría dar algunos consejos sobre por qué los cálculos impuros en Haskell se modelan como mónadas?

Quiero decir que mónada es solo una interfaz con 4 operaciones, entonces, ¿cuál fue el razonamiento para modelar los efectos secundarios?

Supongamos que una función tiene efectos secundarios. Si tomamos todos los efectos que produce como parámetros de entrada y salida, entonces la función es pura para el mundo exterior.

Entonces, para una función impura

f' :: Int -> Int

agregamos el mundo real a la consideración

f :: Int -> RealWorld -> (Int, RealWorld)
-- input some states of the whole world,
-- modify the whole world because of the side effects,
-- then return the new world.

entonces fes puro de nuevo. Definimos un tipo de datos parametrizados type IO a = RealWorld -> (a, RealWorld), por lo que no necesitamos escribir RealWorld tantas veces, y solo podemos escribir

f :: Int -> IO Int

Para el programador, manejar un RealWorld directamente es demasiado peligroso, en particular, si un programador obtiene un valor de tipo RealWorld, podría intentar copiarlo , lo que es básicamente imposible. (Piense en tratar de copiar todo el sistema de archivos, por ejemplo. ¿Dónde lo colocaría?) Por lo tanto, nuestra definición de IO también encapsula los estados de todo el mundo.

Composición de funciones "impuras"

Estas funciones impuras son inútiles si no podemos encadenarlas. Considerar

getLine     :: IO String            ~            RealWorld -> (String, RealWorld)
getContents :: String -> IO String  ~  String -> RealWorld -> (String, RealWorld)
putStrLn    :: String -> IO ()      ~  String -> RealWorld -> ((),     RealWorld)

Queremos

• obtener un nombre de archivo de la consola,
• lee ese archivo y
• imprime el contenido de ese archivo en la consola.

¿Cómo lo haríamos si pudiéramos acceder a los estados del mundo real?

printFile :: RealWorld -> ((), RealWorld)
printFile world0 = let (filename, world1) = getLine world0
                       (contents, world2) = (getContents filename) world1 
                   in  (putStrLn contents) world2 -- results in ((), world3)

Vemos un patrón aquí. Las funciones se llaman así:

...
(<result-of-f>, worldY) = f               worldX
(<result-of-g>, worldZ) = g <result-of-f> worldY
...

Entonces podríamos definir un operador ~~~para vincularlos:

(~~~) :: (IO b) -> (b -> IO c) -> IO c

(~~~) ::      (RealWorld -> (b,   RealWorld))
      ->                    (b -> RealWorld -> (c, RealWorld))
      ->      (RealWorld                    -> (c, RealWorld))
(f ~~~ g) worldX = let (resF, worldY) = f worldX
                   in g resF worldY

entonces podríamos simplemente escribir

printFile = getLine ~~~ getContents ~~~ putStrLn

sin tocar el mundo real

"Impurificación"

Ahora supongamos que también queremos que el contenido del archivo esté en mayúscula. Las mayúsculas son una función pura

upperCase :: String -> String

Pero para llegar al mundo real, tiene que devolver un IO String. Es fácil levantar tal función:

impureUpperCase :: String -> RealWorld -> (String, RealWorld)
impureUpperCase str world = (upperCase str, world)

Esto se puede generalizar:

impurify :: a -> IO a

impurify :: a -> RealWorld -> (a, RealWorld)
impurify a world = (a, world)

para que impureUpperCase = impurify . upperCasepodamos escribir

printUpperCaseFile = 
    getLine ~~~ getContents ~~~ (impurify . upperCase) ~~~ putStrLn

_{(Nota: normalmente escribimos getLine ~~~ getContents ~~~ (putStrLn . upperCase) )}

Estuvimos trabajando con mónadas todo el tiempo.

Ahora veamos lo que hemos hecho:

1. Definimos un operador (~~~) :: IO b -> (b -> IO c) -> IO cque encadena dos funciones impuras juntas
2. Definimos una función impurify :: a -> IO aque convierte un valor puro en impuro.

Ahora hacemos la identificación (>>=) = (~~~)y return = impurify, ¿y vemos? Tenemos una mónada.

Nota tecnica

Para asegurarse de que sea realmente una mónada, todavía hay algunos axiomas que también deben verificarse:

1. return a >>= f = f a

    impurify a                =  (\world -> (a, world))
   (impurify a ~~~ f) worldX  =  let (resF, worldY) = (\world -> (a, world )) worldX 
                                 in f resF worldY
                              =  let (resF, worldY) =            (a, worldX)       
                                 in f resF worldY
                              =  f a worldX

2. f >>= return = f

   (f ~~~ impurify) worldX  =  let (resF, worldY) = f worldX 
                               in impurify resF worldY
                            =  let (resF, worldY) = f worldX      
                               in (resF, worldY)
                            =  f worldX

3. f >>= (\x -> g x >>= h) = (f >>= g) >>= h

   A la izquierda como ejercicio.

¿Alguien podría dar algunos consejos sobre por qué los cálculos impuros en Haskell se modelan como mónadas?

Esta pregunta contiene un malentendido generalizado. La impureza y la mónada son nociones independientes. La impureza no es modelada por Monad. Por el contrario, hay algunos tipos de datos, como IO, que representan el cálculo imperativo. Y para algunos de esos tipos, una pequeña fracción de su interfaz corresponde al patrón de interfaz llamado "Monad". Además, no se conoce una explicación pura / funcional / denotativa de IO(y es poco probable que haya una, teniendo en cuenta el propósito de "sin bin"IO ), aunque existe la historia comúnmente contada sobre World -> (a, World)el significado de IO a. Esa historia no puede describir la verdadIO , porqueIOadmite concurrencia y no determinismo. La historia ni siquiera funciona cuando se trata de cálculos deterministas que permiten la interacción de computación media con el mundo.

Para más explicaciones, vea esta respuesta .

Editar : al volver a leer la pregunta, no creo que mi respuesta esté bastante encaminada. Los modelos de cómputo imperativo a menudo resultan ser mónadas, tal como dice la pregunta. El autor de la pregunta podría no suponer realmente que la mónada de ninguna manera permite modelar el cálculo imperativo.

Según tengo entendido, alguien llamado Eugenio Moggi notó por primera vez que una construcción matemática previamente oscura llamada "mónada" podría usarse para modelar efectos secundarios en lenguajes de computadora y, por lo tanto, especificar su semántica usando el cálculo Lambda. Cuando se estaba desarrollando Haskell, había varias formas en que se modelaban los cálculos impuros ( para más detalles, ver el papel de la "camisa de pelo" de Simon Peyton Jones ), pero cuando Phil Wadler introdujo mónadas rápidamente se hizo evidente que esta era la respuesta. Y el resto es historia.

¿Alguien podría dar algunos consejos sobre por qué los cálculos impuros en Haskell se modelan como mónadas?

Bueno, porque Haskell es puro . Necesita un concepto matemático para distinguir entre cálculos no puros y puros a nivel de tipo y para modelar flujos de programa respectivamente.

Esto significa que tendrá que terminar con algún tipo IO aque modele un cálculo impuro. Luego, debe conocer las formas de combinar estos cálculos que se aplican en secuencia ( >>=) y levantar un valor ( return) son los más obvios y básicos.

Con estos dos, ya has definido una mónada (sin siquiera pensarlo);)

Además, las mónadas proporcionan abstracciones muy generales y potentes , por lo que muchos tipos de flujo de control pueden generalizarse convenientemente en funciones monádicas como sequence, liftMo sintaxis especial, lo que hace que la impureza no sea un caso tan especial.

Vea mónadas en programación funcional y tipificación única (la única alternativa que conozco) para obtener más información.

Como dices, Monades una estructura muy simple. La mitad de la respuesta es: Monades la estructura más simple que podríamos dar a las funciones de efectos secundarios y poder usarlas. Con Monadpodemos hacer dos cosas: podemos tratar un valor puro como un valor de efecto secundario ( return), y podemos aplicar una función de efecto secundario a un valor de efecto secundario para obtener un nuevo valor de efecto secundario ( >>=). Perder la capacidad de hacer cualquiera de estas cosas sería paralizante, por lo que nuestro tipo de efectos secundarios debe ser "al menos" Monad, y resulta que Monades suficiente para implementar todo lo que hemos necesitado hasta ahora.

La otra mitad es: ¿cuál es la estructura más detallada que podríamos dar a los "posibles efectos secundarios"? Ciertamente, podemos pensar en el espacio de todos los posibles efectos secundarios como un conjunto (la única operación que requiere es membresía). Podemos combinar dos efectos secundarios haciéndolos uno tras otro, y esto dará lugar a un efecto secundario diferente (o posiblemente el mismo, si el primero fue "apagar la computadora" y el segundo fue "escribir archivo", entonces el resultado de componer estos es solo "apagar la computadora").

Ok, entonces, ¿qué podemos decir sobre esta operación? Es asociativo; es decir, si combinamos tres efectos secundarios, no importa en qué orden hagamos la combinación. Si lo hacemos (escribir archivo, luego leer socket) y luego apagar la computadora, es lo mismo que hacer escribir archivo luego (leer socket y luego apagar computadora). Pero no es conmutativo: ("escribir archivo" y luego "eliminar archivo") es un efecto secundario diferente de ("eliminar archivo" y luego "escribir archivo"). Y tenemos una identidad: el efecto secundario especial "sin efectos secundarios" funciona ("sin efectos secundarios" y luego "eliminar archivo" es el mismo efecto secundario que "eliminar archivo"). En este punto, cualquier matemático está pensando "¡Grupo!" Pero los grupos tienen inversas, y no hay forma de invertir un efecto secundario en general; "borrar archivo" Es irreversible. Entonces, la estructura que nos queda es la de un monoide, lo que significa que nuestras funciones de efectos secundarios deberían ser mónadas.

¿Hay una estructura más compleja? ¡Por supuesto! Podríamos dividir los posibles efectos secundarios en efectos basados ​​en el sistema de archivos, efectos basados ​​en la red y más, y podríamos llegar a reglas de composición más elaboradas que preserven estos detalles. Pero, de nuevo, todo se reduce a: Monades muy simple y, sin embargo, lo suficientemente potente como para expresar la mayoría de las propiedades que nos interesan. (En particular, la asociatividad y los otros axiomas nos permiten probar nuestra aplicación en piezas pequeñas, con la confianza de que los efectos secundarios de la aplicación combinada serán los mismos que la combinación de los efectos secundarios de las piezas).

En realidad, es una forma bastante clara de pensar en E / S de una manera funcional.

En la mayoría de los lenguajes de programación, realiza operaciones de entrada / salida. En Haskell, imagine escribir código no para realizar las operaciones, sino para generar una lista de las operaciones que le gustaría realizar.

Las mónadas son una sintaxis bonita para eso exactamente.

Si desea saber por qué las mónadas en lugar de otra cosa, supongo que la respuesta es que son la mejor manera funcional de representar las E / S en las que las personas podrían pensar cuando estaban haciendo Haskell.

AFAIK, la razón es poder incluir controles de efectos secundarios en el sistema de tipos. Si quiere saber más, escuche esos episodios de SE-Radio : Episodio 108: Simon Peyton Jones en Programación funcional y Haskell Episodio 72: Erik Meijer en LINQ

Arriba hay respuestas muy buenas y detalladas con antecedentes teóricos. Pero quiero dar mi opinión sobre IO mónada. No soy un programador experimentado de Haskell, por lo que puede ser bastante ingenuo o incluso incorrecto. Pero me ayudó a tratar con IO mónada hasta cierto punto (tenga en cuenta que no se relaciona con otras mónadas).

Primero quiero decir que ese ejemplo con "mundo real" no es muy claro para mí, ya que no podemos acceder a sus estados anteriores (del mundo real). Puede ser que no se relacione con los cálculos de mónada en absoluto, pero se desea en el sentido de transparencia referencial, que generalmente se presenta en el código haskell.

Por eso queremos que nuestro lenguaje (haskell) sea puro. Pero necesitamos operaciones de entrada / salida ya que sin ellas nuestro programa no puede ser útil. Y esas operaciones no pueden ser puras por su naturaleza. Entonces, la única forma de lidiar con esto es separar las operaciones impuras del resto del código.

Aquí viene la mónada. En realidad, no estoy seguro de que no pueda existir otra construcción con propiedades similares necesarias, pero el punto es que la mónada tiene estas propiedades, por lo que puede usarse (y se usa con éxito). La propiedad principal es que no podemos escapar de ella. La interfaz de mónada no tiene operaciones para deshacerse de la mónada en torno a nuestro valor. Otras mónadas (no IO) proporcionan tales operaciones y permiten la coincidencia de patrones (por ejemplo, Quizás), pero esas operaciones no están en la interfaz de la mónada. Otra propiedad requerida es la capacidad de encadenar operaciones.

Si pensamos en lo que necesitamos en términos de sistema de tipos, llegamos al hecho de que necesitamos escribir con constructor, que puede envolverse alrededor de cualquier valle. El constructor debe ser privado, ya que prohibimos escapar de él (es decir, la coincidencia de patrones). Pero necesitamos una función para poner valor en este constructor (aquí el retorno viene a la mente). Y necesitamos el camino para encadenar las operaciones. Si lo pensamos por algún tiempo, llegaremos al hecho de que la operación de encadenamiento debe tener un tipo como >> = has. Entonces, llegamos a algo muy similar a la mónada. Creo que si ahora analizamos posibles situaciones contradictorias con esta construcción, llegaremos a los axiomas de la mónada.

Tenga en cuenta que la construcción desarrollada no tiene nada en común con la impureza. Solo tiene propiedades, que deseamos tener para poder manejar operaciones impuras, a saber, no escapar, encadenar y una forma de entrar.

Ahora, un conjunto de operaciones impuras está predefinido por el idioma dentro de esta mónada IO seleccionada. Podemos combinar esas operaciones para crear nuevas operaciones impuras. Y todas esas operaciones tendrán que tener IO en su tipo. Sin embargo, tenga en cuenta que la presencia de IO en el tipo de alguna función no hace que esta función sea impura. Pero, según tengo entendido, es una mala idea escribir funciones puras con IO en su tipo, ya que inicialmente fue nuestra idea separar las funciones puras e impuras.

Finalmente, quiero decir que la mónada no convierte las operaciones impuras en puras. Solo permite separarlos de manera efectiva. (Repito, es solo mi entendimiento)