[Agda] Re: Agda FFI bindings

[Benja Fallenstein]

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?

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.

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