[Agda] sequencing 3 IO operations

[Alan Jeffrey]

I hit the same problem, and ended up redefining the IO datatype to make 
 >> and >>= inductive rather than coinductive, and adding an additional 
rec coinductive constructor.  This tidies up all of the regular 
sequencing code, at the expense of an additional knot-tying constructor 
each time a non-wellfounded recursion is used.

A.

On 08/27/2010 04:54 PM, Jeremy Shaw wrote:
> Hello,
>
> I realize I am in uncharted territory here, but I am wondering how to
> improve the sequencing of three IO operations. If you have:
>
> foo2 : IO ⊤
> foo2 =
>      ♯ putStrLn "foo 1">>
>      ♯ putStrLn "foo 2"
>
> Everything is fine. But if you try to extend it to three:
>
> foo3 : IO ⊤
> foo3 =
>      ♯ putStrLn "foo 1">>
>      ♯ putStrLn "foo 2">>
>      ♯ putStrLn "foo 3"
>
> It does not typecheck.
> If we look at the definition for>>:
>
> data IO : Set → Set₁ where
>     lift   : ∀ {A} (m : Prim.IO A) → IO A
>     return : ∀ {A} (x : A) → IO A
>     _>>=_  : ∀ {A B} (m : ∞ (IO A)) (f : (x : A) → ∞ (IO B)) →
> IO B
>     _>>_   : ∀ {A B} (m₁ : ∞ (IO A)) (m₂ : ∞ (IO B)) → IO B
>
>
> we see that>>  returns an IO B value. So we can't do
>
>     (♯ a>>  ♯ b)>>  ♯ c
>
> Instead we need an extra, ♯
>
>    ♯ (♯ a>>  ♯ b)>>  ♯ c
>
> Well, that gets ugly pretty fast. Is there any obvious work around ?
>
> Here is a complete example (using Agda and lib from darcs head):
> module IOIOIO where
>
> open import Coinduction using (♯_)
> open import Data.Unit using (⊤)
> open import IO using (IO; _>>_; putStrLn; run)
> import IO.Primitive as Prim
>
> foo4 : IO ⊤
> foo4 =
>      ♯ putStrLn "foo 1">>
>      ♯ (♯ putStrLn "foo 2">>
>         ♯ (♯ putStrLn "foo 3">>
>            ♯ putStrLn "foo 4"))
>
> main : Prim.IO ⊤
> main = run foo4_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda