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

[Alan Jeffrey]

Thanks for the pointer!  More bedtime reading for me...

A.

On 10/04/2010 03:25 PM, Nils Anders Danielsson wrote:
> 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