[Agda] Re: Agda FFI bindings

Brandon Moore brandon_m_moore at yahoo.com
Tue Sep 21 22:59:26 CEST 2010

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



More information about the Agda mailing list