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

La IOmónada en Haskell a menudo se explica como una mónada estatal donde el estado es el mundo. Entonces, un valor de tipo IO amónada se ve como algo así worldState -> (a, worldState).

Hace algún tiempo leí un artículo (o una publicación de blog / lista de correo) que criticaba esta opinión y daba varias razones por las que no es correcta. Pero no puedo recordar ni el artículo ni las razones. ¿Cualquiera sabe?

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

Editar: El artículo que estaba buscando es Abordar el equipo incómodo: entrada / salida monádica, concurrencia, excepciones y llamadas en idioma extranjero en Haskell por Simon Peyton Jones. (Gracias a la respuesta de TacTics).

El problema IO a = worldState -> (a, worldState)es que si esto fuera cierto, podríamos demostrarlo forever (putStrLn "Hello") :: IO ay undefined :: IO aser 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))

Lema: (\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 undefinedson programas equivalentes. Sin embargo, claramente no deben considerarse programas equivalentes, en teoría o en la práctica.

Tenga en cuenta que este modelo es incorrecto incluso sin invocar concurrencia.

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

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

http://comonad.com/reader/2011/free-monads-for-less-3/

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

Ver Tackling the Awkward Squad .

La gran razón es que los modelos de estado RealWorld de la mónada IO no funcionan bien con la concurrencia. SPJ en este clásico legible favorece el uso de una semántica operativa para entenderlo.

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

El código correspondiente a esto está en Hackage como IOSpec: http://hackage.haskell.org/package/IOSpec

Creo que la tesis de Wouter entra en más detalles: http://www.staff.science.uu.nl/~swier004/Publications/Thesis.pdf