[Agda] Re: Agda FFI bindings

[Nils Anders Danielsson]

On 2010-09-17 16:30, Alan Jeffrey wrote:
> So my temptation is to focus on inductive, rather than coinductive
> bindings to Haskell.
>
> Thoughts?

The FFI is inherently unsafe (it is easy to prove bottom using it), so
it falls on the people writing FFI bindings to ensure that the Agda
interfaces are safe to use. Whether this should be restricted to the
compile-time behaviour (no undefined : (A : Set) → A), or also include
run-time behaviour, can be discussed. The standard library's IO module
does not prevent the raising of exceptions, for instance.

--
/NAD