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

[Alan Jeffrey]

It's not just random values, it's full on random behaviour, notably 
random blocking (and possibly random exceptions depending on the 
treatment of exceptions).  This could be handled by a monad, but the 
difference between that monad and the IO monad would be pretty slim, so 
you may as well use the IO monad for it.  Which brings us back to 
Lennart's proposal of an IO monad with strict semantics.

A.

On 09/22/2010 05:32 AM, Christoph Herrmann wrote:
> Hi,
>
> isn't nondeterminism of some values ubiquitous in the presence
> of I/O, also if laziness is not concerned?
> We would expect that calling a random number generator will
> result in (pseudo) random values, and when such a
> value is output, the observational behaviour will differ between runs.
>
> Would Agda not provide the chance to clearly separate by type
> those values which come from the outside world and those which
> result purely from the logics of the program?
>
> If the aim is to extend purity to an entire system, maybe involving
> different processors, communication channels and hard drives,
> then a special build-in monad seems to be necessary. Even then,
> purity would require healthiness of all involved devices and
> efforts to achieve a sufficient degree of fault tolerance in practice.
>
> Best regards
>
> On 22 Sep 2010, at 09:10, 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.
>>
>> (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
>>>
>>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
> --
>   Dr. Christoph Herrmann
>   University of St Andrews, Scotland/UK
>   phone: office: +44 1334 461629, home: +44 1334 478648
>   email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
>   URL:   http://www.cs.st-andrews.ac.uk/~ch
>
>   The University of St Andrews is a charity registered in Scotland: No SC013532
>
>
>
>