[Agda] Re: Agda FFI bindings

[Nils Anders Danielsson]

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?

This has already been discussed, I believe.

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

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

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

--
/NAD