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

[Alan Jeffrey]

Can you say a bit about why this approach is better than a plain old 
monad?  Why is it better to be parametric in C, R and translateLocal 
rather than fix:

   C = \exists IO
   R (X , io) = X
   translateLocal (X , io) = io

?  Also, monads (or premonoidal categories if you prefer) have a nice 
categorical presentation, could you say how to interpret your 
construction categorically?

A.

On 09/22/2010 02:27 PM, Anton Setzer wrote:
> On 22/09/10 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
>>
>
> I agree that something is broken with the IO as it is in Haskell, it really
> behaves strangely when using files.
> I did some research with peter Hancock and came to the solution that
> an interface of an IO program should be given by a set of commands
> C and a set of return values to this comment R : C ->  Set.
> Then an IO program can be given by issueing a command
> to the real world (an element c of type C and depending on the
> response of the world (an element Rc) issues the next command,
> or terminates (if one wants a monad) with an element of the return type.
>
> This guarantees a strict order between inputs and outputs, namely
> the program can only issue a response once it has issued a command,
> and after the response the next command is issued.
> For file handling one can read the file one piece at a time,
> and depending it write to a different file. If one wants to get
> the content of a file as a string, one would need to issue a command
> which in one go reads the complete file. One can model
> more sophisticated behaviour, but that needs to be done while interacting
> with a transparent IO interface.
>
> See the articles with Peter hancock on my homepage
>
> http://www.cs.swan.ac.uk/~csetzer/
>
> and the implementation of a graphics library and a drawing program
> at
>
>   http://www-compsci.swan.ac.uk/~csetzer/software/agda2/IOLib/
>
> Anton
>
>> 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
>>
>
>