[Agda] Re: Agda FFI bindings

[Nicolas Pouillard]

On Tue, 5 Oct 2010 08:48:36 -0500, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
> 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 :-)

Then you want to either fail when the file is too long, but how much?
Or take the length as argument.

And this does not solve the issue with stdin (interactive usage).

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

If you want that performing an (IO A) always terminate then I would suggest
to give this monad another name. Haskell people will be highly confused to
see that. Indeed the Haskell IO monad is a sinkbin, however while we can
design a lot of smaller monads for various purposes, the need for combining
them is real. It leads to lifting all of them to only one which we used to
call IO.

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

Lazy IO is dangerous in the general cases, but there is plenty of cases
perfectly fine. A simple one is `interact', in Agda I would expect.

interact : (Costring → Costring ⊥) → TheDoItAllMonad ()

Best regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr