# New Foreign Function Interface¶

Ever since Idris has had multiple backends compiling to different target languages on potentially different platforms, we have had the problem that the foreign function interface (FFI) was written under the assumption of compiling to C. As a result, it has been hard to write generic code for multiple targets, or even to be sure that if code compiles that it will run on the expected target.

As of 0.9.17, Idris will have a new foreign function interface (FFI) which is aware of multiple targets. Users who are working with the default code generator can happily continue writing programs as before with no changes, but if you are writing bindings for an external library, writing a back end, or working with a non-C back end, there are some things you will need to be aware of, which this page describes.

## The IO' monad, and main¶

The IO monad exists as before, but is now specific to the C backend (or, more precisely, any backend whose foreign function calls are compatible with C.) Additionally, there is now an IO' monad, which is parameterised over a FFI descriptor:

data IO' : (lang : FFI) -> Type -> Type


The Prelude defines two FFI descriptors which are imported automatically, for C and JavaScript/Node, and defines IO to use the C FFI and JS_IO to use the JavaScript FFI:

FFI_C  : FFI
FFI_JS : FFI

IO : Type -> Type
IO a = IO' FFI_C a

JS_IO : Type -> Type
JS_IO a = IO' FFI_JS a


As before, the entry point to an Idris program is main, but the type of main can now be any implementation of IO', e.g. the following are both valid:

main : IO ()
main : JS_IO ()


The FFI descriptor includes details about which types can be marshalled between the foreign language and Idris, and the “target” of a foreign function call (typically just a String representation of the function’s name, but potentially something more complicated such as an external library file or even a URL).

## FFI descriptors¶

An FFI descriptor is a record containing a predicate which holds when a type can be marshalled, and the type of the target of a foreign call:

record FFI where
constructor MkFFI
ffi_types : Type -> Type
ffi_fn : Type


For C, this is:

||| Supported C integer types
public export
data C_IntTypes : Type -> Type where
C_IntChar   : C_IntTypes Char
C_IntNative : C_IntTypes Int
C_IntBits8  : C_IntTypes Bits8
C_IntBits16 : C_IntTypes Bits16
C_IntBits32 : C_IntTypes Bits32
C_IntBits64 : C_IntTypes Bits64

||| Supported C function types
public export
data C_FnTypes : Type -> Type where
C_Fn : C_Types s -> C_FnTypes t -> C_FnTypes (s -> t)
C_FnIO : C_Types t -> C_FnTypes (IO' FFI_C t)
C_FnBase : C_Types t -> C_FnTypes t

||| Supported C foreign types
public export
data C_Types : Type -> Type where
C_Str   : C_Types String
C_Float : C_Types Double
C_Ptr   : C_Types Ptr
C_MPtr  : C_Types ManagedPtr
C_Unit  : C_Types ()
C_Any   : C_Types (Raw a)
C_FnT   : C_FnTypes t -> C_Types (CFnPtr t)
C_IntT  : C_IntTypes i -> C_Types i

||| A descriptor for the C FFI. See the constructors of C_Types
||| and C_IntTypes for the concrete types that are available.
%error_reverse
public export
FFI_C : FFI
FFI_C = MkFFI C_Types String


This is the example of linking C code.

%include C "mylib.h"


Example Makefile

DEFAULT: mylib.o main.idr
idris main.idr -o executableFile

clean:
rm -f executableFile mylib.o main.ibc


## Foreign calls¶

To call a foreign function, the foreign function is used. For example:

do_fopen : String -> String -> IO Ptr
do_fopen f m
= foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m


The foreign function takes an FFI description, a function name (the type is given by the ffi_fn field of FFI_C here), and a function type, which gives the expected types of the remaining arguments. Here, we’re calling an external function fileOpen which takes, in the C, a char* file name, a char* mode, and returns a file pointer. It is the job of the C back end to convert Idris String to C char* and vice versa.

The argument types and return type given here must be present in the fn_types predicate of the FFI_C description for the foreign call to be valid.

Note The arguments to foreign must be known at compile time, because the foreign calls are generated statically. The %inline directive on a function can be used to give hints to help this, for example a shorthand for calling external JavaScript functions:

%inline
jscall : (fname : String) -> (ty : Type) ->
{auto fty : FTy FFI_JS [] ty} -> ty
jscall fname ty = foreign FFI_JS fname ty


### C callbacks¶

It is possible to pass an Idris function to a C function taking a function pointer by using CFnPtr in the function type. The Idris function is passed to MkCFnPtr in the arguments. The example below shows declaring the C standard library function qsort which takes a pointer to a comparison function.

myComparer : Ptr -> Ptr -> Int
myComparer = ...

qsort : Ptr -> Int -> Int -> IO ()
qsort data elems elsize = foreign FFI_C "qsort"
(Ptr -> Int -> Int -> CFnPtr (Ptr -> Ptr -> Int) -> IO ())
data elems elsize (MkCFnPtr myComparer)


There are a few limitations to callbacks in the C FFI. The foreign function can’t take the function to make a callback of as an argument. This will give a compilation error:

-- This does not work
example : (Int -> ()) -> IO ()
example f = foreign FFI_C "callbacker" (CFnPtr (Int -> ()) -> IO ()) f


Note that the function that is used as a callback can’t be a closure, that is it can’t be a partially applied function. This is because the mechanism used is unable to pass the closed-over values through C. If we want to pass Idris values to the callback we have to pass them through C explicitly. Non-primitive Idris values can be passed to C via the Raw type.