[Agda] First cut of semantics-preserving IO bindings

[Alan Jeffrey]

Hi everyone,

Look, over on github!

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

This is a first shot at IO bindings that respect Agda's semantics.  If 
you recall back on this thread:

   http://thread.gmane.org/gmane.comp.lang.agda/1949

The problem is that Haskell's lazy IO breaks eta-equivalence on lists, 
and so doesn't respect Agda's semantics (which allows eta-equivalent 
functions to be proved extensionally equivalent).

We could just use strict IO, but then any programs which process 
streaming data would either have to buffer all their input, or would 
have to be rewritten to use the IO monad rather than be pure, even 
though they're not doing any IO.

I proposed:

   http://thread.gmane.org/gmane.comp.lang.agda/1949/focus=1980

adopting an IO model with commitment points, where all externally 
visible IO is buffered until a commit is reached.  For example, Hello 
World is:

   putStr "Hello, World\n" >> commit

This allows us to have strict semantics, but eat our cake lazily.  For 
example, a program which discards its input runs in constant space, even 
when fed a 500M file:

      559,216,832 bytes allocated in the heap
           91,624 bytes copied during GC
           20,392 bytes maximum residency (1 sample(s))
           33,296 bytes maximum slop
                2 MB total memory in use (0 MB lost due to fragmentation)

Its strict equivalent has to buffer all input, and doesn't GC any.

There are, of course, a lot of issues left untouched, e.g. 
exception-handling, whether we need rollback as well as commit, worries 
about multiple sparks/threads/processes, lack of atomicity for commit, 
etc. etc. etc., but I think the basic transactional IO model is a sound one.

A.