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

[wren ng thornton]

On 10/5/10 5:56 PM, Alan Jeffrey wrote:
> There are, however, examples where I don't see how to program them in
> the iteree model, for example:
>
> main =
> getContents >>= \x
> let xml = parseXML x in
> let xml' = transformXML xml in
> putStr (serializeXML xml')
>
> Imagining that transformXML implements a tree automaton, this should run
> in space proportional to the height of the tree. I'm not sure I see how
> to implement this as an iteree (without rewriting transformXML, e.g.
> differentiate the type of XML documents, and use a Huet zipper, or
> resorting to callcc).

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

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.

-- 
Live well,
~wren