[Agda] Agda FFI bindings

Alan Jeffrey ajeffrey at bell-labs.com
Thu Sep 16 21:40:44 CEST 2010


Dear Agda folks,

I've been working on some Agda applications, which have made a fair bit 
of use of the FFI to Haskell, and I thought it might make sense to 
share.  Currently I've got simple bindings for:

- Data.Maybe
- Data.ByteString.Lazy
- Text.XML.Expat
- Network.URI
- Data.Int.Int64

Is there currently a home for such bindings?  If not, I'd like to start 
one up.  If anyone else has FFI bindings to share, I'd be happy to 
provide a home for them.

Before I start uploading code, I'd like to ask a bit about coding style. 
  The style I've been using so far has been to define two modules:

- Foreign.Haskell.Foo: contains just the raw FFI bindings
- Foo: links against Foreign.Haskell.Foo, and provides the Agda layer.

Is this good practice?  Or should I just include the FFI code in with 
the Agda library?

There are many gory questions about the particular FFIs, but I'll put 
those off for the moment :-)

Best wishes,

Alan.


More information about the Agda mailing list