[Agda] Agda FFI bindings

[Anton Setzer]

Just one comment. My library which allowed to write a drawing program in
Agda based on a proper implementation of a IO made extensive use
of the FFI, and allows to write programs for graphical applications
(open a window, draw lines and rectangles there, interact with the mouse).

It is available at

http://www-compsci.swan.ac.uk/~csetzer/software/agda2/IOLib/


Anton

On 16/09/10 20:40, Alan Jeffrey wrote:
> 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 r
> - 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------