[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

True, but it's not obvious that this semantics is captured any better by 
Costring than by String.  There's a bypass of the type system going on 
in the Haskell interface for getContents; the "real" type for 
getContents is IO (IOList Char) where

   data IOList A : Set where
     [] : IOList A
     _::_ : A -> IO (IOList A) -> IOList A

that is, after reading some content, there is still IO to be performed. 
  Haskell (for perfectly sensible pragmatic reasons) hides this IO under 
the hood and pretends it isn't happening.  This produces some weird 
results, such as making eta-equivalent functions distinguishable, since:

   do
     s <- getContents
     putStr (f s)

will block waiting for input if f touches its argument, and print 
immediately otherwise.

In Haskell this doesn't matter much, as eta-equivalence isn't 
extensional anyway, due to divergence and error, but is somewhat 
troubling for Agda.

Eta-equivalence holds just as much for Costrings as it does for Strings, 
so I still don't see what is being bought by having getContents return a 
Costring rather than a String.

Lack of eta-equivalence is caused by semi-closed handles -- anything 
which leaves the handle in an open or closed state is fine, such as getLine.

A.

On 09/21/2010 03:59 PM, Brandon Moore 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?
>
> I know very little about codata or the FFI in agda, but
> files can include named pipes, and stranger things
> under /proc, and of course the full Handle interface
> covers sockets and stdio.
>
> If readFile is producing codata, writeFile should
> definitely consume it, in case it is not possible
> to parse input from the colist into inductive
> data, or if you want to stream out infinite output
> (for that strongly typed implementation of "yes").
>
> Brandon
>
>
>
>