[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

On 09/21/2010 05:42 PM, Benja Fallenstein wrote:
> Hi Alan,
>
> On Wed, Sep 22, 2010 at 12:16 AM, Alan Jeffrey<ajeffrey at bell-labs.com>  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?
>>>
>>> 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 :-)
>
> Quite true, but I suppose the question is whether we want potentially
> infinitely interacting programs to be typed as recursive, even though
> we think of the job they do as a corecursive thing?

Yes, but we're doing this all inside an IO wrapper, and the IO type 
itself includes partiality / nontermination.  I think of (IO String) as 
giving a weak safety result: if the program terminates successfully, it 
returns a finite string.  Since any terminated program only uses finite 
time, this is the same as saying that it returns an acyclic string.

So I'd say it's OK [er, modulo stuff with semi-closed handles, see other 
post] to have IO claim to have a recursive type as long as it never 
generates any cycles.

> I.e., I'd say if we think of using readFile with an infinite stream as
> a normal thing rather than as the user kind of abusing the system,
> then it seems appropriate to me to use codata, even though it wouldn't
> be dangerous to use data instead. But if we see readFile as being
> there to be used on files, even though it could also be naughtily used
> on infinite streams, it'd feel sensible to make it return data, not
> codata.

What are these infinite streams of which you speak :-)  I only see 
finite streams that haven't closed yet.

> - Benja
>
> P.S. This doesn't affect me directly, though, since I haven't yet
> graduated into the elect class of people who actually run their Agda
> programs instead of merely typechecking them :-)

Computing is an Experimental Science :-)

A.