[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

OK, my first problem in FFI bindings to Haskell: what's the treatment of 
binding to recursive datatypes and functions?  (There's a matching 
problem of nonterminating computation and error, but lets ignore that 
for now.  Ditto unsoundness of postulates.)

As a concrete example, take the List datatype and its append function 
(ignoring for now that Agda has its own perfectly good append function).

Currently, Foreign.Haskell gives a binding for Haskell lists as Agda 
Colists, so the Agda binding for append is:

   append : {X : Set} -> (Colist X) -> (Colist X) -> (Colist X)

This can be wrapped in a conversion function from lists to colists, but 
there's nothing we can do to convert the result back a list, without 
switching off termination checking.

An alternative would be to do what Data.String does for strings, and 
bind Haskell lists to Agda Lists, which gives append the desired type:

   append : {X : Set} -> (List X) -> (List X) -> (List X)

then it's the responsibility of the author of the library with FFI 
bindings to ensure that all such bindings maintain finiteness.

Note that in both cases there's a responsibility on the author: in the 
case of bindings to coinductive types, it's to maintain guardedness, and 
in the case of bindings to inductive types, it's to maintain finiteness.

We could do both, although this would probably end up with either a fair 
bit of code duplication or complex types to track inductive vs 
coinductive types.

Finally, we could just say that the author is allowed whatever bindings 
they like, and is not required to maintain any invariants, but this 
sounds like a recipe for cryptic MAlonzo error messages.

Having hacked out a bunch of code built on top of Haskell FFI libraries 
recently, I've found the inductive bindings to be extremely useful, and 
have yet to use any coinductive bindings.  Of course, this may say more 
about me than it does about common programming idioms :-)

So my temptation is to focus on inductive, rather than coinductive 
bindings to Haskell.

Thoughts?

A.

On 09/16/2010 02:40 PM, Jeffrey, Alan S A (Alan) 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
> - 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.