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

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.

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>     

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'.

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.

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