[Agda] Announcement: Agda FFI

[Nils Anders Danielsson]

On Thu, Mar 20, 2008 at 11:33 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
> The darcs version of Agda now has support for a simple Haskell FFI, which
> allows any Haskell function to be called from Agda. The documentation is on
> the wiki:
>
> http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Docs.FFI

Nice, we need a foreign function interface.

Given the way Alonzo works I presume that type errors in pragmas can
easily lead to undefined behaviour, including segmentation faults,
right? If this is the case I suggest that we warn about it on the wiki
page. (In the future one might hope for somewhat stronger guarantees,
but this is a good start.)

The FFI should probably be seen as a _low-level_ tool to interface to
other languages and libraries, just like in Haskell. If used carefully
it can be used to build executable, dependently typed abstractions of
various real-world concepts. And I can start writing my shell scripts
in Agda. :)

-- 
/NAD