Crítica da mônada IO sendo vista como uma mônada de estado operando no mundo

O problema com IO a = worldState -> (a, worldState) é que, se isso fosse verdade, poderíamos provar que forever (putStrLn "Hello") :: IO a e undefined :: IO a são iguais. Aqui está a prova cortesia 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
  =
⊥

Portanto, forever m = fix (\r -> \w -> r (snd $ m w)) = ⊥

Em particular, forever (putStrLn "Hello") = ⊥ e, consequentemente, forever (putStrLn "Hello") e undefined são programas equivalentes. No entanto, claramente eles não devem ser considerados programas equivalentes, na teoria ou na prática.

Observe que esse modelo está errado mesmo sem invocar a simultaneidade.

Aqui está uma resposta trivial: qualquer mudança no estado da mônada do estado é devido a quaisquer ações executadas na mônada. Se de fato o "WorldState - > (a, WorldState) ”explicação reivindica a mesma propriedade, com WorldState sendo um valor puro que somente a mônada IO muda, está errado. Mudanças de horário, o conteúdo dos arquivos, o estado das alças, etc. podem mudar independentemente do que acontece na mônada IO. Esse é o ponto da mônada IO. O fato de que o GHC passa em torno de um valor RealWorld (ou w / e foi) abaixo é para garantir que as coisas são executadas em ordem, tanto quanto eu sei, se isso (pode ser apenas algo para colocar no valor de ST). p>     

Eu escrevi uma postagem no blog sobre o tópico de como modelar IO como uma forma de co-rotina assimétrica se comunicando com o sistema de tempo de execução para o seu idioma. (É admitidamente a terceira parte de uma série)

link

Esse post aborda um pouco do motivo pelo qual é esquisito raciocinar sobre a semântica da "passagem pelo mundo".

Veja Enfrentando o esquadrão inábil .

O grande motivo é que os modelos de estado RealWorld da IO môn não funcionam bem com a simultaneidade. O SPJ neste clássico legível favorece o uso de uma semântica operacional para entendê-lo.

O código correspondente a isso está no Hackage como IOSpec: link

Acho que a tese de Wouter é mais detalhada: link