164 votos

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

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

¿Mónada es solo una interfaz con 4 operaciones, ¿cuál fue el razonamiento de modelar los efectos secundarios en ella?

286voto

KennyTM Puntos 232647

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

Así, para una impuro función

f' :: Int -> Int

añadimos 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 a side effects,
-- then return the new world.

a continuación, f es puro otra vez. Definimos un parametrizar el tipo de datos IO a = RealWorld -> (a, RealWorld), por lo que no necesitamos tipo de mundo real muchas veces

f :: Int -> IO Int

Para el programador, el manejo de un mundo real directamente es demasiado peligroso-en particular, si un programador pone sus manos en un valor de tipo mundo real, puede que intenten copiar , que es básicamente imposible. (Pensar en intentar copiar el sistema de archivos entero, por ejemplo. ¿Dónde te pongo?) Por lo tanto, nuestra definición de IO encapsula los estados de todo el mundo.

Estos impuro funciones son inútiles si no podemos cadena de ellos juntos. Considere la posibilidad de

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, leer ese archivo, a continuación, imprimir el contenido. ¿Cómo podemos hacerlo si nos puede acceder el mundo real de los estados?

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

Podemos ver un patrón aquí: se llama a las funciones como este:

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

Así podríamos definir un operador ~~~ a ellos se unen:

(~~~) :: (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

a continuación, simplemente se podría escribir

printFile = getLine ~~~ getContents ~~~ putStrLn

sin tocar el mundo real.


Ahora supongamos que queremos crear el archivo de contenido mayúsculas también. Poner en mayúsculas es una pura función

upperCase :: String -> String

Pero para hacerlo en el mundo real, tiene que devolver un IO String. Es fácil levantar una función de este tipo:

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

esto puede ser generalizado:

impurify :: a -> IO a

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

así que impureUpperCase = impurify . upperCase, y podemos escribir

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

(Nota: Normalmente escribimos getLine ~~~ getContents ~~~ (putStrLn . upperCase))


Ahora vamos a ver lo que hemos hecho:

  1. Hemos definido un operador (~~~) :: IO b -> (b -> IO c) -> IO c que las cadenas de dos impuro de funciones
  2. Hemos definido una función impurify :: a -> IO a que se convierte en un puro valor a lo impuro.

Ahora hacemos la identificación (>>=) = (~~~) y return = impurity, y de ver? Tenemos una monada.


(Para comprobar si es realmente una monada hay pocos axiomas deben ser satisfechos:

(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) a worldX = let (resF, worldY) = impuify a worldX 
                              in f resF worldY
                            = let (resF, worldY) = (a, worldX)     
                              in f resF worldY
                            = f a worldX

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

Ejercicio.)

43voto

Conal Puntos 9874

Alguien podría dar algunas pistas sobre por qué el unpure cálculos en Haskell son modelados como mónadas?

Esta pregunta contiene un malentendido generalizado. La impureza y la Mónada son independientes de las nociones. La impureza es no modelado por la Mónada. Más bien, hay un par de tipos de datos, tales como IO, que representan el imperativo de la computación. Y para algunos de esos tipos, una pequeña fracción de su interfaz corresponde a la interfaz patrón llamado "Mónada". Por otra parte, no se conoce puro/funcional/denotativa explicación de IO (y no es poco probable, teniendo en cuenta el "sin bin" propósito de IO), aunque no es la que comúnmente se contó la historia sobre World -> (a, World) siendo el significado de IO a. Esa historia no puede con la verdad describir IO, porque IO admite la concurrencia y no determinismo. La historia no funciona aún cuando para determinista cálculos que permiten a mediados de la computación de la interacción con el mundo.

Para obtener una explicación más detallada, vea esta respuesta.

Edit: En la re-lectura de la pregunta, no creo que mi respuesta es bastante en la pista. Modelos de imperativo de cálculo, no suelen llegar a ser mónadas, así como la pregunta dice. El autor de la pregunta no podría realmente asumir que monadness de alguna manera permite el modelado de imperativo de cálculo.

13voto

Paul Johnson Puntos 8604

Como yo lo entiendo, alguien llamó a Eugenio Moggi notó por primera vez que un oscuro con anterioridad construcción matemática se llama una "mónada" podría ser utilizado para el modelo de efectos secundarios en lenguajes de ordenador, y por lo tanto, especificar su semántica mediante cálculo Lambda. Cuando Haskell estaba siendo desarrollado, fueron varias las formas en que los impuros cálculos fueron modeladas (ver Simon Peyton Jones' "hair shirt" de papel para obtener más detalles), pero cuando Phil Wadler introducido mónadas rápidamente se hizo evidente que esta era La Respuesta. Y el resto es historia.

8voto

Dario Puntos 26259

Alguien podría dar algunas pistas sobre por qué el unpure cálculos en Haskell son modelados como mónadas?

Bien, debido a que Haskell es puro. Usted necesita un concepto matemático para distinguir entre unpure cálculos y puros en el tipo de nivel y el modelo de programación de los flujos respectivamente.

Esto significa que usted tendrá que terminan con algún tipo IO a que los modelos de un unpure la computación. Entonces usted necesita saber la manera de combinar los cálculos de las que se aplican en la secuencia (>>=) y levantar un valor (return) son las más obvias y básicas.

Con estos dos, que ya ha definido una mónada (sin pensarlo);)

Además, las mónadas proporcionar muy general y potente abstracciones, por lo que muchos de los tipos de control de flujo puede ser convenientemente generalizada en monádico funciones como sequence, liftM o sintaxis especial, haciendo unpureness no es un caso especial.

Ver mónadas en la programación funcional y la singularidad de escribir (la única alternativa que yo sepa) para obtener más información.

3voto

Gabriel Ščerbák Puntos 7982

Que yo sepa, la razón es poder incluir efectos secundarios los controles en el sistema. Si usted quiere saber más, escuchar esos episodios SE-Radio : episodio 108: Simon Peyton Jones sobre la programación funcional y Haskell episodio 72: Erik Meijer en LINQ

Iteramos.com

Iteramos es una comunidad de desarrolladores que busca expandir el conocimiento de la programación mas allá del inglés.
Tenemos una gran cantidad de contenido, y también puedes hacer tus propias preguntas o resolver las de los demás.

Powered by:

X