[Agda] Re: Agda FFI bindings

[Brandon Moore]

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

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

Brandon