[Agda] sequencing 3 IO operations

[Nils Anders Danielsson]

On 2010-08-27 22:54, Jeremy Shaw wrote:
> Well, that gets ugly pretty fast. Is there any obvious work around ?

It's linear in the number of operations, so it isn't that bad:

   foo5 : IO ⊤
   foo5 =                   ♯
     putStrLn "foo 1" >> ♯ (♯
     putStrLn "foo 2" >> ♯ (♯
     putStrLn "foo 3" >> ♯ (♯
     putStrLn "foo 4" >> ♯
     putStrLn "foo 5"      )))

Note that the current definition of IO is somewhat problematic, because
it allows the definition of non-productive loops:

   loop = ♯ return 0 >> ♯ loop

You could use the Hancock/Setzer approach to IO instead. With this
approach you can guarantee absence of non-productive loops, assuming
that you can guarantee that all primitive commands are productive.

--
/NAD