[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

On 09/21/2010 04:28 PM, kahl at cas.mcmaster.ca wrote:
> Hi Alan,
>
>   >  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?
>
> We have to be, since many (conceptually) infinite streams are available via
> the filesystem abstraction, for example named pipes (mkfifo(3)).

True, but you can only tell that the FFI writer has broken their 
contract after the stream has produced an infinite amount of data, and 
I'm not holding my breath waiting for that to happen :-)

A.