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

[Nils Anders Danielsson]

On 2010-09-24 04:07, Alan Jeffrey wrote:
> If I can get this up and running, then adding a little bit of dependency
> to ensure that IO is being used safely should be quite routine. Hooray,
> Agda IO which is comparable in space usage to Haskell IO, but has the
> same semantics as strict IO.

Some Haskellers which dislike lazy IO seem to be quite keen on
"iteratees". I don't know too much about them, but you may want to have
a look:

   http://okmij.org/ftp/Streams.html
   http://www.google.co.uk/search?q=iteratees

--
/NAD