[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

On 10/04/2010 03:17 PM, Nils Anders Danielsson 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.

OK, so they can be merged if/when the FFI can cope with universe 
polymorphism.

>
>> 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?
>
> This has already been discussed, I believe.

Indeed.

>> 3. Since the \inf type is erased at compile-time, do we still need to
>> distinguish between Primitive.IO and IO? We could just add a postulate
>> inf : forall {A} ->  \inf(IO A) ->  (IO A) which compiles to the identity
>> function.
>
> IO.Primitive.IO is the Haskell IO type, IO.IO is a type describing
> potentially non-terminating IO computations.

Yes, that I get, I just don't understand why not just include a 
postulate inf : forall {A} ->  \inf(IO A) ->  (IO A), and get rid of the 
distinction between IO.Primitive.IO and IO.IO.  At the moment, the 
regular uses of IO.IO end up cluttered with hashes and flats, which is 
quite painful, compared to a simple knot-tying postulate.

>> 4. Currently, the erasure of the \inf type is treated specially by the
>> compiler -- couldn't we just add COMPILED and COMPILED_TYPE pragmas to
>> perform the erasure?
>
> No, because the compiler doesn't handle universe polymorphism.

See 1 above.

>> 5. Is there a test suite to ensure correct run-time behaviour of the
>> standard library?
>
> No, except possibly for some unit tests in the code (of the form
> test : e₁ ≡ e₂; test = refl). The library includes a number of proofs,
> though. The FFI-using code cannot be tested "internally", and I have not
> set up a good test-suite for it.

OK, hence my queasiness about submitting patches to the compiler :-)

> --
> /NAD

A.