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

[Alan Jeffrey]

OK, first pass on the bedtime reading done.

There's a lot of similarity between iteratees and Anton's resumption 
model.  Ignoring a lot of gorey details for the moment, the basic type 
of an iteree with return type A and alphabet X is:

   M = A + (X -> M)

which is isomorphic to:

   M = A + (1 x (X -> M))

i.e. a resumption model with trivial output type.

Moreover, there's an obvious extension of DFAs to handle a case of 
output, in pseudo-Agda:

   record DFA-with-output (X A : Set) : Set1 where
     field Q : Set
     field q0 : Q
     field A : (Pred Q)
     field accept : (q : Q) -> (Dec (q \in A))
     field next : (q : Q) -> (q \nin A) -> X -> Q

And (not that I've checked the details, but...) there should be mappings 
back and forth between resumptions and DFAs-with-output.

Iterees then build on this to give a parser-combinator-on-steroids 
library.  There are things which are much nicer in this model, for 
example consider a simple wc application, which with Lazy IO would be:

   main =
     getContents >> \ x ->
     putStr ("length: " ++ length x ++ ", words: " ++ length (words x))

This program is very nice, but has a horrible space leak caused by 
copying x, which (AFAICT) is tricky to fix within the lazy IO model 
without resorting to sparks, callcc, unsafePerformIO or some such.

The iteree model is driven by the data producer, so the equivalent of 
the above runs in constant space, at the cost of requiring length and 
words to be written in the iteree monad.

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

So I can certainly see that an iteree / resumption / parser combinator 
model is necessary, but I'm not sure that everything should be forced 
into its mold.  I'm still quite tempted to explore a transactional IO model.

A.

On 10/04/2010 04:57 PM, Jeffrey, Alan S A (Alan) wrote:
> 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
>