NewFFI

The problem with the current FFI

The current FFI in Agda is not very convenient to use:

    postulate head : forall {a} {A : Set a} -> List A -> a
    {-# COMPILED_UHC head (\_ _ -> Data.List.head) #-}
    {-# COMPILED head (\_ _ -> Data.List.head) #-}

The programmer is responsible for dropping the Level/Set arguments before calling the Haskell function, which can easily lead to wrong code. Also, the above code cannot be inspected or generated using reflection (at the moment).

Design space

FFI specification

We need a description of the foreign function we want to call. This normally contains some form of name, a type and optionally some additional information (e.g. safe/unsafe).

The name and additional information can easily be represented by an Agda record:

    record C-FFICall : Set where
        field
          name : String
          isSafe : Bool -- does the C code call Agda/HS callbacks

However, it's not clear how the type should be represented. The two choices are either:

Define the universe of C/HS/JS types using an Agda datatype

    data τ-Hs : Set where
      var : (k : ℕ) → τ-Hs
      app : τ-Hs → τ-Hs → τ-Hs
      ∀'  : τ-Hs → τ-Hs
      _=>_ : τ-Hs → τ-Hs → τ-Hs
      -- An agda name with the same runtime representation as a Haskell type
      ty  : (nm-Agda : Name) → τ-Hs

Example:

    haskell type:  forall a . a -> a
    ffi type specification: ∀' (var 0 => var 0)
    derived Agda type: {A : Level} -> {a : Set A} -> a -> a

The advantage of this approach is that the ffi spec is easily inspectable. The main disadvantage is that the syntax is likely going to be more verbose.

For simple type signatures, Agda probably can also infer the τ-Hs given an Agda type. For polymorphic types Agda is probably not going to be able to so by itself, however this could be worked around using Reflection. This doesn't look like a simple and elegant solution to me though.

See also: http://idris.readthedocs.org/en/latest/reference/ffi.html , http://anil.recoil.org/papers/drafts/2015-cmeleon-icfp-draft1.pdf

Use normal Agda types

Example:

    haskell type:  forall a . a -> a
    ffi type specification: {a : Set} -> List a -> List a

The big advantage here is that Agda's type syntax is quite nice, and we can just use it as is. The compiler will have to check that the given type is a valid FFI type, but that check should be rather straightforward.

FFI-Calls and multiple compile targets / operating systems

We may want to build libraries targeting multiple compile backends, e.g. Haskell and JS. This means that we have to provide the appropriate FFI calls for each compile target. To make matters worse, even for the same compile target the foreign binding may differ for different platforms (win/unix/mac).

This is a hard problem, and while there are some better and worse approaches, it's not clear what's the best choice.

Some options:

• CPP-style Preprocessor (e.g. Haskell)

  • + Simple
  • - Only active configuration is type-checked, other code ignored
• Allow one foreign call expression to have binding for multiple compile targets

  • + Allows type-checking everything
  • - Only works if all foreign bindings have the exact same type
  • - Doesn't work if the code for different compile targets uses different foreign calls/primitives

As the solution is not clear, I'm just going to ignore this problem for now and will assume we just want to add FFI-Calls targeting *one* compile target/platform/operating system.

Top-level definitions or expressions

Should foreign calls be top-level definitions or expressions?

Allowing foreign calls to be expressions is more general, and should go well together with reflection. It would allow Reflection to easily generate foreign calls. For compilation, foreign call expressions can just be lifted to top-level definitions if necessary.

Proposed solution

I propose to add a new expression for foreign calls, which takes a datatype containing the naming information and an Agda type to create a FFI call:

    data FFISpec : Set where
      HS-Call : String -> FFISpec
      C-Call : String -> Safety -> FFISpec

    foreign : FFISpec -> (x: Set) -> x

The "foreign" keyword would behave somewhat similar to "unquote", and would require it's arguments to be closed terms. The keyword may be used in any arbitrary expressions, or at the top-level as well:

    f : _
    f = foreign (HS-Call "Prelude.id") ({a : Set} -> a -> a)

To implement this, foreign calls either need to be translated internally to the current Axiom-approach or the Internal syntax needs to be extended.