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

[Alan Jeffrey]

OMG, it's the early 1990s all over again :-)

On 09/22/2010 03:10 AM, Lennart Augustsson wrote:
> 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.

Unsurprisingly, I agree.  The semantics of Agda IO should be strict -- 
there may be some cleverness we can do under the hood with buffering 
output to allow an implementation in terms of lazy IO, but that 
shouldn't be exposed to the Agda programmer.

> (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₂.)

You can prove a lot of equivalences in the one point domain :-)

>    -- Lennart

A.

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