Crítica de la mónada IO vista como una mónada estatal que opera en el mundo

45

La mónada IO en Haskell a menudo se explica como una mónada estatal donde el estado es el mundo. Por lo tanto, un valor del tipo IO a monad se ve como algo así como worldState -> (a, worldState) .

Hace algún tiempo leí un artículo (o un blog / publicación de la lista de correo) que criticó esta opinión y dio varias razones por las que no es correcto. Pero no puedo recordar ni el artículo ni las razones. Alguien sabe?

Editar: El artículo parece perdido, así que comencemos a recopilar varios argumentos aquí. Estoy empezando una recompensa para hacer las cosas más interesantes.

Edit: El artículo que estaba buscando es Enfrentando al equipo incómodo: entrada / salida monádica, concurrencia, excepciones y llamadas a idiomas extranjeros en Haskell por Simon Peyton Jones. (Gracias a la respuesta de TacTics.)

    
pregunta Petr Pudlák 20.08.2012 - 09:33

5 respuestas

30

El problema con IO a = worldState -> (a, worldState) es que si esto fuera cierto, podríamos probar que forever (putStrLn "Hello") :: IO a y undefined :: IO a son iguales. Aquí está la prueba cortesía de dolio (2010, irc):

forever m
 =
m >> forever m
 =
fix (\r -> m >> r)
 = {definition of >> for worldState -> (a, worldState)}
fix (\r -> \w -> r (snd $ m w))

Lemma: (\r w -> r (snd $ m w)) ⊥ = ⊥

(\r w -> r (snd $ m w)) ⊥
  =
\w -> ⊥ (snd $ m w))
  =
⊥ . snd . m
  =
⊥

Por lo tanto, forever m = fix (\r -> \w -> r (snd $ m w)) = ⊥

En particular, forever (putStrLn "Hello") = ⊥ y, por lo tanto, forever (putStrLn "Hello") y undefined son programas equivalentes. Sin embargo, claramente no deben considerarse programas equivalentes, ni en teoría ni en la práctica.

Observe que este modelo es incorrecto incluso sin invocar la concurrencia.

    
respondido por el Russell O'Connor 05.09.2012 - 21:51
12

Aquí hay una respuesta trivial: cualquier cambio en el estado de la mónada estatal se debe a cualquier acción que se haya ejecutado en la mónada. Si de hecho el "WorldState - > (a, WorldState) ”la explicación reclama la misma propiedad, siendo WorldState un valor puro que solo la mónada IO cambia, está mal. Los cambios de hora, el contenido de los archivos, el estado de los manejadores, etc. pueden cambiar independientemente de lo que suceda en la mónada IO. Ese es el punto de la mónada IO. El hecho de que GHC transmita un valor de RealWorld (o w / e era) debajo es garantizar que las cosas se ejecuten en orden, por lo que sé, si eso (puede ser algo para poner en el valor de ST). p>     

respondido por el Christopher Done 04.09.2012 - 16:43
11

Escribí una publicación de blog sobre el tema de cómo modelar IO como una forma de comunicación de coroutine asimétrica con el sistema de tiempo de ejecución para su idioma. (Es cierto que es la tercera parte de una serie)

enlace

Esa publicación cubre un poco de por qué es incómodo razonar acerca de la semántica de 'pasar por el mundo'.

    
respondido por el Edward KMETT 04.09.2012 - 18:18
8

Consulte Abordando al escuadrón torpe .

El motivo principal es que los modelos de estado real de la mónada IO no funcionan bien con la concurrencia. SPJ en este clásico legible favorece el uso de una semántica operacional para entenderlo.

    
respondido por el TacTics 04.09.2012 - 18:25
5

La queja principal sobre los modelos de estado de RealWorld es que, como dice TacTics, el paso del mundo no necesariamente funciona con la concurrencia. Pero Wouter Swierstra y Thorsten Altenkirch demostraron cómo razonar acerca de la concurrencia como un efecto de "paso del mundo", con una secuencia fija pero arbitraria de hilos de entrelazado en su artículo "La bella en la bestia: una semántica funcional para el escuadrón torpe": < a href="http://www.staff.science.uu.nl/~swier004/Publications/BeautyInTheBeast.pdf"> enlace

El código correspondiente a esto está en Hackage como IOSpec: enlace

Creo que la tesis de Wouter entra en más detalles: enlace

    
respondido por el sclv 04.09.2012 - 18:37

Lea otras preguntas en las etiquetas