[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

As promised, here's the patch to the standard library...

It adds FFI bindings for Empty, List, Maybe, Stream and Sum.

It doesn't add FFI bindings to:

- Unit: is a record, so can't be translated.
- Vec and co: are dependent, so can't be translated.
- Product: are dependent records, so can't be translated.
- Colist: I'm confused as to why there are currently two Colist types.
- Nat, Integer and co: need more thought about good numeric bindings.

In particular, List, Maybe and Either show up in many many many Haskell 
APIs, so binding them to Agda's List, Maybe and Sum types should help a 
lot with Haskell-Agda interoperability.

A.

On 09/21/2010 02:33 PM, Jeffrey, Alan S A (Alan) wrote:
> I'm working on a patch to the standard library to introduce more FFI
> bindings.  Some questions this kicked up...
>
> 1. Why are there two Colist dataypes?  (One's in Foreign.Haskell, and
> one's in Data.Colist.)
>
> 2. Why do the functions readFile, writeFile etc. produce / take
> Costrings rather than Strings?  Are we really worried that there are
> infinitely long files on disk?
>
> 3. Since the \inf type is erased at compile-time, do we still need to
> distinguish between Primitive.IO and IO?  We could just add a postulate
> inf : forall {A} ->  \inf(IO A) ->  (IO A) which compiles to the identity
> function.
>
> 4. Currently, the erasure of the \inf type is treated specially by the
> compiler -- couldn't we just add COMPILED and COMPILED_TYPE pragmas to
> perform the erasure?
>
> 5. Is there a test suite to ensure correct run-time behaviour of the
> standard library?  The only test of the runtime I could find is in
> test/compiler/Main.agda, which tests trustMe.
>
> Back to patching...
>
> A.
>
> On 09/20/2010 08:34 PM, Jeffrey, Alan S A (Alan) wrote:
>> 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: StdLibFFI.patch
Type: text/x-patch
Size: 25867 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100921/cad2b0d2/StdLibFFI-0001.bin