[Agda] Re: Agda FFI bindings

kahl at cas.mcmaster.ca kahl at cas.mcmaster.ca
Tue Sep 21 23:28:11 CEST 2010


Hi Alan,

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


Wolfram



More information about the Agda mailing list