Critica della monade IO considerata come una monade di stato che opera nel mondo

Il problema con IO a = worldState -> (a, worldState) è che se ciò fosse vero, potremmo provare che forever (putStrLn "Hello") :: IO a e undefined :: IO a sono uguali. Ecco la prova per gentile concessione di 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
  =
⊥

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

In particolare forever (putStrLn "Hello") = ⊥ e quindi forever (putStrLn "Hello") e undefined sono programmi equivalenti. Tuttavia, chiaramente non dovrebbero essere considerati programmi equivalenti, in teoria o in pratica.

Si noti che questo modello è sbagliato anche senza invocare la concorrenza.

Ecco una risposta banale: qualsiasi modifica allo stato della monade di stato è dovuta a qualsiasi azione eseguita nella monade. Se davvero il "WorldState - > (a, WorldState) "la spiegazione rivendica la stessa proprietà, con WorldState che è un valore puro che solo la monade IO cambia, è sbagliato. I cambiamenti di orario, il contenuto dei file, lo stato delle maniglie, ecc. Possono cambiare indipendentemente da ciò che accade nella monade IO. Questo è il punto della monade IO. Il fatto che GHC passi attorno a un valore di RealWorld (o che lo fosse) è garantire che le cose siano in ordine, per quanto ne so, se questo (potrebbe essere solo qualcosa da inserire nel valore ST).

Ho scritto un post sul blog su come modellare IO come una forma di coroutine asimmetrica che comunica con il sistema di runtime per la tua lingua. (È certamente la terza parte di una serie)

link

Quel post copre un po 'il motivo per cui è scomodo ragionare sulla semantica del "passaggio del mondo".

Vedi Affrontare la Squadra Impressionante .

La grande ragione è che i modelli di stato RealWorld della monade IO non funzionano bene con la concorrenza. SPJ in questo leggibile classico favorisce l'utilizzo di una semantica operativa per comprenderlo.

La lamentela principale sui modelli di stato RealWorld è che, come dice TacTics, il passaggio del mondo non necessariamente funziona con la concorrenza. Ma Wouter Swierstra e Thorsten Altenkirch hanno mostrato come ragionare sulla concorrenza come effetto "world-passing", con una sequenza fissa ma arbitraria di thread interleaving nel loro paper "Beauty in the Beast: A Functional Sematics for the Awkward Squad": < a href="http://www.staff.science.uu.nl/~swier004/Publications/BeautyInTheBeast.pdf"> link

Il codice corrispondente a questo è su Hackage come IOSpec: link

Penso che la tesi di Wouter vada più nel dettaglio: link