[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

Here's a patch which implements the changes discussed below.  It enables 
FFI bindings which mention universe-polymorphic types such as Data.Maybe 
and Data.List.

Alan.

PS: Should I create an enhancement request on the bugtracker?

PPS: If you include the patch, please add "Alcatel-Lucent" to the list 
of authors in the LICENSE file.  Thanks!

On 09/20/2010 01:34 PM, Jeffrey, Alan S A (Alan) wrote:
> 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.
>>
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: UniversePolymorphismFFI.patch
Type: text/x-patch
Size: 62351 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100920/f3e50f4d/UniversePolymorphismFFI-0001.bin