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.