[Agda] IO, semi-closed handles, and problems with extensional equality

[Lennart Augustsson]

I think Agda should abandon lazy IO (and thus semi-closed handles).
They are a constant source of nuisance in Haskell and programs using
them can only be explained by assuming that the IO monad gives totally
random results.  You can explain them in the same way in Agda, I guess
but it's not pretty.

(Here's the argument why program₁ and program₂ can behave differently
even if they are equivalent:
Anything happening in the IO monad is random, so running program₁
twice can result if different behaviour.
So even if program₁ ≡ program₂ you can't expect running program₁
necessarily giving the same result as program₂.)

  -- Lennart

On Wed, Sep 22, 2010 at 4:30 AM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
> Hi everyone,
>
> Starting a new thread, since we've stopped talking about FFIs a while ago.
>  Old thread is here:
>
>  http://article.gmane.org/gmane.comp.lang.agda/1936
>
> I kicked the hornets nest and asked why IO is based on Costring rather than
> String.  It seems to me that the culprit is semi-closed handles in Haskell,
> as described here:
>
>  http://www.haskell.org/onlinelibrary/io.html#sect21.2.2
>
> "[After a call to hGetContents hdl], hdl is effectively closed, but items
> are read from hdl on demand and accumulated in a special list returned by
> hGetContents hdl."
>
> AFAICT, this is the underlying source of laziness in the IO library, the
> other functions return results strictly, for example there's no problem with
> hGetLine having the Agda type (Handle -> IO String) as it waits until a NL
> before returning a fully evaluated string.
>
> The discussion around IO and lazy strings made me realize there's a question
> as to what the goals for the IO library should be.  I will posit an
> innocent-looking goal, and then give a counterexample using the current IO
> bindings :-)
>
>  GOAL:
>  Extensionally equivalent programs have the same runtime behaviour.
>
> Obviously this is an informal goal, as the Haskell runtime system isn't
> formalized, but at least we can do experiments.  For example, here are a
> couple of programs which do not have the same runtime behaviour:
>
> -- This program blocks until it receives input
>
> hello₁ : Costring → IO Unit
> hello₁ []       = putStrLn (fromString "hello")
> hello₁ (x ∷ xs) = putStrLn (fromString "hello")
>
> program₁ : IO Unit
> program₁ = getContents >>= hello₁
>
> -- This program prints immediately
>
> hello₂ : Costring → IO Unit
> hello₂ x = putStrLn (fromString "hello")
>
> program₂ : IO Unit
> program₂ = getContents >>= hello₂
>
> For extensional equivalence, I should probably define a proper equivalence
> on IO, which includes the monad laws, but for right now I'll do a hack and
> extend propositional equivalence with a postulate expressing that >>= is a
> congruence (note, wrt extensional equivalence on the right):
>
>  postulate _⟨>>=⟩_ :
>    {A B : Set} → {io₁ io₂ : IO A} → {f₁ f₂ : A → IO B} →
>      (io₁ ≡ io₂) → (∀ a → f₁ a ≡ f₂ a) →
>        (io₁ >>= f₁) ≡ (io₂ >>= f₂)
>
> Unfortunately, it is easy to show that (program₁ ≡ program₂), thus giving a
> counterexample to the goal.  (The proof uses the snapshot 2.2.7 compiler,
> but can probably be munged to go through in 2.2.6).
>
> Possible fixes:
>
> a) Abandon the goal (er, so what's the point of mechanized proof then?)
>
> b) Abandon semi-closed handles (ouch, buffering inefficencies!)
>
> c) Er, something really clever I've not thought of.
>
> Thoughts?
>
> A.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>