haskell io monads

haskell - ¿En qué sentido es pura la IO Mónada?



monads (8)

He tenido la mónada IO descrita para mí como una mónada estatal donde el estado es "el mundo real". Los defensores de este enfoque de IO argumentan que esto hace que las operaciones de IO sean puras, como referencialmente transparentes. ¿Porqué es eso? Desde mi perspectiva, parece que el código dentro de la mónada IO tiene muchos efectos secundarios observables. Además, ¿no es posible describir casi cualquier función no pura como una función del mundo real? Por ejemplo, ¿no podemos pensar, digamos, en malloc de C como una función que toma un RealWorld y un Int y devuelve un puntero y un RealWorld , solo como en la mónada de IO que el RealWorld está implícito?

Nota: sé lo que es una mónada y cómo se usa. No respondas con un enlace a un tutorial aleatorio de mónadas a menos que se dirija específicamente a mi pregunta.

Además, ¿no es posible describir casi cualquier función no pura como una función del mundo real? Por ejemplo, ¿no podemos pensar, digamos, en malloc de C como una función que toma un RealWorld y un Int y devuelve un puntero y un RealWorld, solo como en la mónada de IO que el RealWorld está implícito?

Sin lugar a duda ...

La idea general de la programación funcional es describir los programas como una combinación de pequeños cálculos independientes que generan cálculos más grandes.

Al contar con estos cálculos independientes , obtendrá muchos beneficios, desde programas concisos hasta códigos paralelizables eficientes y eficientes, holgazanería hasta la rigurosa garantía de que el control fluya como se espera, sin posibilidad de interferencia o corrupción de datos arbitrarios.

Ahora , en algunos casos (como IO), necesitamos un código impuro. Los cálculos que involucran tales operaciones no pueden ser independientes, podrían mutar los datos arbitrarios de otro cálculo.

El punto es que Haskell siempre es puro , IO no cambia esto.

Entonces, nuestros códigos impuros e independientes tienen que obtener una dependencia común: tenemos que aprobar un RealWorld . Entonces, sea cual sea el cálculo con estado que queremos ejecutar, tenemos que pasar este RealWorld para aplicar nuestros cambios a, y cualquier otro cálculo con estado que quiera ver o hacer cambios tiene que conocer el RealWorld también.

Si esto se hace explícita o implícitamente a través de la mónada IO es irrelevante. Desarrollas un programa Haskell como un computo gigante que transforma datos, y una parte de estos datos es el RealWorld .

Una vez que se llama al main :: IO () inicial cuando se ejecuta su programa con el mundo real actual como parámetro, este mundo real se lleva a cabo a través de todos los cálculos impuros involucrados, tal como lo haría un State en un State . Eso es de lo que se vale monadic >>= (bind).

Y donde el RealWorld no obtiene (como en los cálculos puros o sin ningún >>= -ing en main ), no hay posibilidad de hacer nada con él. Y donde lo consigue, eso sucedió por el paso puramente funcional de un parámetro (implícito). Es por eso

let foo = putStrLn "AAARGH" in 42

no hace absolutamente nada, y por qué la mónada IO , como cualquier otra cosa, es pura. Lo que sucede dentro de este código puede, por supuesto, ser impuro, pero todo está atrapado dentro, sin posibilidad de interferir con cálculos no conectados.

Bueno, esto es lo que nos enseñaron en la universidad:

La función es referencialmente transparente cuando siempre devuelve el mismo valor para la entrada especificada (o la misma expresión siempre evalúa el mismo valor en el mismo contexto). Por lo tanto, por ejemplo, getChar no sería referencialmente transparente si tuviera la firma de tipo just () -> Char o Char , porque puede obtener diferentes resultados si llama a esta función varias veces con el mismo argumento.

Pero, si introduce la mónada IO, entonces getChar puede tener tipo IO Char y este tipo tiene solo un valor único: IO Char . Entonces getChar siempre getChar generar el mismo valor, sin importar qué usuario clave realmente presionó.

Pero aún puede "obtener" el valor subyacente de esta cosa IO Char . Bueno, realmente no se obtiene, sino que se pasa a otra función usando el operador de vinculación ( >>= ), para que pueda trabajar con el Char que el usuario ingresó más en su programa.

Dejaré que Martin Odersky responda esto

La mónada IO no hace una función pura. Simplemente hace que sea obvio que es impuro.

Suena lo suficientemente claro.

El inventor de Mónadas dice: En un lenguaje impuro, una operación como tic estaría representada por una función de tipo () -> (). El argumento espurio () es necesario para retrasar el efecto hasta que se aplique la función, y dado que el tipo de salida es () uno puede adivinar que el propósito de la función radica en un efecto secundario. Por el contrario, aquí el tic tiene el tipo M (): no se necesita argumento espurio, y la aparición de M indica explícitamente qué tipo de efecto puede ocurrir .

No entiendo cómo M () hace que la lista de argumentos vacíos, (), sea menos espuria, pero Wadler es bastante claro en cuanto a que las Mónadas solo indican un tipo de efecto secundario, no lo eliminan . Los seguidores de Haskel parecen engañarnos a nosotros mismos cuando afirman que las mónadas eliminan la impureza.

Simplemente se reduce a la igualdad extensional :

Si getLine llamar a getLine dos veces, ambas llamadas devolverían una IO String que se vería exactamente igual en el exterior cada vez. Si tuviera que escribir una función para tomar 2 IO String y devolver un Bool para señalar una diferencia detectada entre ambas, no sería posible detectar ninguna diferencia de ninguna propiedad observable. No podría preguntar a ninguna otra función si son iguales y cualquier intento de usar >>= también debe devolver algo en IO que todos son iguales externamente .

Supongamos que tenemos algo como:

animatePowBoomWhenHearNoiseInMicrophone :: TimeDiff -> Sample -> IO () animatePowBoomWhenHearNoiseInMicrophone levelWeightedAverageHalfLife levelThreshord = ... programA :: IO () programA = animatePowBoomWhenHearNoiseInMicrophone 3 10000 programB :: IO () programB = animatePowBoomWhenHearNoiseInMicrophone 3 10000

Aquí hay un punto de vista:

animatePowBoomWhenHearNoiseInMicrophone es una función pura en el sentido de que sus resultados para la misma entrada, programA y programB , son exactamente iguales. Puedes hacer main = programA o main = programB y sería exactamente lo mismo.

animatePowBoomWhenHearNoiseInMicrophone es una función que recibe dos argumentos y que da como resultado una descripción de un programa. El tiempo de ejecución de Haskell puede ejecutar esta descripción si establece main en él o si no lo incluye en main través del enlace.

¿Qué es IO ? IO es una DSL para describir programas imperativos, codificados en estructuras y funciones de datos "puro-haskell".

"complete-haskell" también conocido como GHC es una implementación de "pure-haskell" y una implementación imperativa de un decodificador / ejecutable de IO .

Creo que la mejor explicación que he escuchado fue realmente hace poco en SO. IO Foo es una receta para crear un Foo . Otra forma común, más literal, de decir esto es que es un "programa que produce un Foo ". Se puede ejecutar (muchas veces) para crear un Foo o morir en el intento. La ejecución de la receta / programa es lo que queremos en última instancia (de lo contrario, ¿por qué escribir uno?), Pero lo que representa una acción IO en nuestro código es la receta misma.

Esa receta es un valor puro, en el mismo sentido exacto que una String es un valor puro. Las recetas pueden combinarse y manipularse de maneras interesantes, a veces asombrosas, pero las muchas formas en que se pueden combinar estas recetas (a excepción de la descaradamente no unsafePerformIO , unsafeCoerce , etc.) son completamente referencialmente transparentes, deterministas y tan agradables cosas. La receta resultante no depende en absoluto del estado de otra cosa que no sean las recetas de las que se creó.