[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

On 10/05/2010 02:56 AM, Nicolas Pouillard 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?
>
> Yes /dev/stdin, /dev/zero, /dev/urandom, many custom file-systems...

Indeed, there are unbounded streams, but I'm not going to hold my breath 
waiting for them to return an infinite amount of data :-)

Typing for IO guarantees weak safety -- a term of type (IO A) guarantees 
that if it terminates, it does so with a value of type A.  Any program 
which terminates must do so having used a finite amount of space, so the 
only source of infinite streams is cyclicity.  So if an IO library can 
guarantee acyclicity of its results, it can return data, not codata.

(And see other thread on why Agda's IO bindings have to have strict 
semantics, not Haskell lazy IO semantics.)

A.