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

45

A IO monad em Haskell é frequentemente explicada como uma monad de estado em que o estado é o mundo. Então, um valor do tipo IO a monad é visto como algo como worldState -> (a, worldState) .

Algum tempo atrás, eu li um artigo (ou um blog / post de lista de discussão) que criticou essa visão e deu várias razões por que não está correto. Mas não me lembro nem do artigo nem das razões. Alguém sabe?

Edit: O artigo parece perdido, então vamos começar a reunir vários argumentos aqui. Estou começando uma recompensa para tornar as coisas mais interessantes.

Edit: O artigo que eu estava procurando é Enfrentando o esquadrão desajeitado: entrada / saída monádica, simultaneidade, exceções e chamadas de idioma estrangeiro no Haskell por Simon Peyton Jones. (Graças à resposta de TacTics.)

    
por Petr Pudlák 20.08.2012 / 09:33
fonte

5 respostas

30

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.

    
por 05.09.2012 / 21:51
fonte
12

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>     

por 04.09.2012 / 16:43
fonte
11

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

    
por 04.09.2012 / 18:18
fonte
8

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.

    
por 04.09.2012 / 18:25
fonte
5
A principal reclamação sobre os modelos de estado do RealWorld é que, como diz o TacTics, a aprovação do mundo não funciona necessariamente com a simultaneidade. Mas Wouter Swierstra e Thorsten Altenkirch mostraram como raciocinar sobre a simultaneidade como um efeito de "passagem do mundo", com uma sequência fixa, mas arbitrária, de tópicos de entrelaçamento em seu artigo "A Bela na Fera: Uma Seática Funcional para o Esquadrão Estranho": href="http://www.staff.science.uu.nl/~swier004/Publications/BeautyInTheBeast.pdf"> link

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

Acho que a tese de Wouter é mais detalhada: link

    
por 04.09.2012 / 18:37
fonte