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

[Anton Setzer]

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
>   


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------