[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

Next problem... universe polymorphism.  There was already a thread on 
this "COMPILED_DATA directive for Maybe":

  http://thread.gmane.org/gmane.comp.lang.agda/1237/

One thing that's not mentioned there is that there actually is a binding 
for the universe-polymorphic Maybe type which typechecks:

  {-# COMPILED_DATA Maybe AMaybe Just Nothing #-}

where AMaybe is a Haskell type defined:

  type AMaybe a b = Maybe b

This is fine, and indeed compiles Agda Maybe into Haskell Maybe. 
Unfortunately, you can't use the type in another FFI binding, for example:

  postulate isJust : {a : Level} → {A : Set a} → (Maybe A) → Bool
  {-# COMPILED isJust isJust #-}
  // The type {a : Level} {A : Set a} → Maybe A → Bool cannot be
  // translated to a Haskell type.

For universe-monomorphic bindings you get a different error:

  postulate isJust : {A : Set zero} → (Maybe A) → Bool
  {-# COMPILED isJust isJust #-}
  // The type zero cannot be translated to a Haskell type.

The source of these errors is HaskellTypes.hs -- it looks like there'd 
be an easy fix for universe-monomorphic bindings, which is to add a 
cluase to haskellType, something like:

   Lit (LitLevel _ _) -> "()"

There's probably a similar hack for polymorphic bindings, by adding a 
case for the BUILTIN_LEVEL datatype to haskellKind.

As NAD said in the previous thread, the best bet right now is to define 
a universe-monomorphic Foreign.Haskell.Maybe type with translations back 
and forth to Data.Maybe {zero}, but boy does this result in a lot of 
ugly wrapper code.

A.

On 09/17/2010 03:30 PM, Jeffrey, Alan S A (Alan) wrote:
> 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.
>