[Agda] Re: Agda FFI bindings

[Peter Hancock]

On 21/09/2010 21:59, Brandon Moore wrote:
>> 2. Why do the functions readFile, writeFile etc. produce / take 
>> Costrings rather than Strings?  Are we really worried that there are 
>> infinitely long files on disk?
> 
> I know very little about codata or the FFI in agda, but
> files can include named pipes, and stranger things
> under /proc, and of course the full Handle interface
> covers sockets and stdio.

Absolutely right.  (Except maybe it's files that are strange,
and devices the norm.)
 
> If readFile is producing codata, writeFile should
> definitely consume it, in case it is not possible
> to parse input from the colist into inductive
> data, or if you want to stream out infinite output
> (for that strongly typed implementation of "yes").

It's not really an important point, but I'm very surprised you
say that readFile as *produces* data rather than *consumes* it
(and conversely for writeFile).  Do you think
of yourself as sitting "in the program"?  Or the environment
it interacts with (like I do)? 

Hank
(An ex-systems programmer.)