[Agda] Re: Agda FFI bindings

[Nicolas Pouillard]

On Mon, 04 Oct 2010 21:17:51 +0100, Nils Anders Danielsson <nad at Cs.Nott.AC.UK> wrote:
> On 2010-09-21 20:33, Alan Jeffrey wrote:
> > 1. Why are there two Colist dataypes? (One's in Foreign.Haskell, and
> > one's in Data.Colist.)
> 
> The one in Data.Colist is universe polymorphic, the other one isn't.
> 
> > 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...

Regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr