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

[Alan Jeffrey]

On 10/05/2010 09:40 PM, wren ng thornton wrote:
> You can't. Or rather, you can't for all possible transformXML without
> breaking the nice resource guarantees that iteratees give you. The proof
> is trivial. The idea of iteratees is based around stream processing; so
> long as you can process the stream incrementally (as you can with `wc`
> and most parsers), then you can produce output with fixed overhead. But
> streams don't support random access or unbounded scanning, so there are
> transformations of sequences which can't but hold onto the entire
> sequence before generating output (or alternatively, re-reading the
> inputs). But that problem isn't anything new: if you need the whole file
> in memory, that's your problem :)

Indeed.  I suspect that there is a hack with callcc that could do the 
trick, and would give O(height) space usage in the case where 
transformXML implements a tree automaton, but it wouldn't be pleasant!

> But, there are other resource guarantees that iteratees give besides
> memory consumption. The most important ones are that it gives you
> control over when resources like filehandles, sockets, and database
> connections are acquired and released. It's these resources which cause
> the big bugs with lazy-IO, and they're far more precious than memory. So
> long as your transformXML function can consume its entire input in a
> timely fashion, we can still guarantee that the filehandle is released
> in a timely fashion. No semi-closed filehandle nonsense.

Indeed.  That's what I'm hoping for over at:

   http://github.com/agda/agda-system-io

The idea is that "commit" guarantees a point at which resources are 
released, so the XML example becomes:

   getContents >>= \x ->
   let xml = parseXML x in
   let xml' = transformXML xml in
   putStr (serializeXML xml') >>
   commit

and it's that final commit that forces the IO to take place, after which 
the input stream is guaranteed to be closed.  Moreover, you can add 
extra commit points if you want more strictness, e.g. to force all XML 
parsing to take place before transformation, you say:

   getContents >>= \x ->
   let xml = parseXML x in
   commit >>
   let xml' = transformXML xml in
   putStr (serializeXML xml') >>
   commit

There's lots of rough edges here though, notably a lack of ACID 
guarantees (not much we can do about that in the absence of a 
transactional filesystem), and lack of rollback or exception handling.

A.