[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

On 10/06/2010 02:55 AM, Nicolas Pouillard wrote:
> 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).

See previous discussion over on this thread:

http://thread.gmane.org/gmane.comp.lang.agda/1949

My proposal is to always give IO strict semantics, but to use hackery 
with commitment points to recover some of the performance benefit of 
lazy io.  First-cut instantiation is on github:

http://github.com/agda/agda-system-io

Strict getContents fails to terminate when applied to an unbounded or 
blocked stream.

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

Er no, I said weak safety, not strong safety, hence "if it terminates".

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

Agreed strongly.  IO is a really bad name for this monad, Computation or 
Interaction or TheDoItAllMonad or DoStuff or T would all be better names 
:-)  Fortunately in Agda we can at least index the monad by an effect 
algebra, but designing that algebra will be hard!

>> (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 ()

The problem is that this function doesn't respect extensional 
equivalence: the example at the beginning of the "IO, semi-closed 
handles, and problems with extensional equality" thread can be adapted 
to use interact rather than raw IO.

AFAICT you can either ditch lazy semantics or eta-equivalence -- I 
choose to ditch lazy semantics!  (Note this is lazy semantics, not lazy 
performance benefits, which we could still aim for.)

A.

 >
 > Best regards,