1******************************
2New Foreign Function Interface
3******************************
5.. sectionauthor:: Edwin Brady
7Ever since Idris has had multiple backends compiling to different
8target languages on potentially different platforms, we have had the
9problem that the foreign function interface (FFI) was written under
10the assumption of compiling to C. As a result, it has been hard to
11write generic code for multiple targets, or even to be sure that if
12code compiles that it will run on the expected target.
14As of 0.9.17, Idris will have a new foreign function interface (FFI)
15which is aware of multiple targets. Users who are working with the
16default code generator can happily continue writing programs as before
17with no changes, but if you are writing bindings for an external
18library, writing a back end, or working with a non-C back end, there
19are some things you will need to be aware of, which this page
22The ``IO'`` monad, and ``main``
23===============================
25The ``IO`` monad exists as before, but is now specific to the C
26backend (or, more precisely, any backend whose foreign function calls
27are compatible with C.) Additionally, there is now an ``IO'`` monad,
28which is parameterised over a FFI descriptor:
32 data IO' : (lang : FFI) -> Type -> Type
34The Prelude defines two FFI descriptors which are imported
35automatically, for C and JavaScript/Node, and defines ``IO`` to use
36the C FFI and ``JS_IO`` to use the JavaScript FFI:
47 JS_IO a = IO' FFI_JS a
49As before, the entry point to an Idris program is ``main``, but the
50type of ``main`` can now be any implementation of ``IO'``, e.g. the
51following are both valid:
58The FFI descriptor includes details about which types can be
59marshalled between the foreign language and Idris, and the "target" of
60a foreign function call (typically just a String representation of the
61function's name, but potentially something more complicated such as an
62external library file or even a URL).
67An FFI descriptor is a record containing a predicate which holds when
68a type can be marshalled, and the type of the target of a foreign
75 ffi_types : Type -> Type
82 ||| Supported C integer types
84 data C_IntTypes : Type -> Type where
85 C_IntChar : C_IntTypes Char
86 C_IntNative : C_IntTypes Int
87 C_IntBits8 : C_IntTypes Bits8
88 C_IntBits16 : C_IntTypes Bits16
89 C_IntBits32 : C_IntTypes Bits32
90 C_IntBits64 : C_IntTypes Bits64
92 ||| Supported C function types
94 data C_FnTypes : Type -> Type where
95 C_Fn : C_Types s -> C_FnTypes t -> C_FnTypes (s -> t)
96 C_FnIO : C_Types t -> C_FnTypes (IO' FFI_C t)
97 C_FnBase : C_Types t -> C_FnTypes t
99 ||| Supported C foreign types
101 data C_Types : Type -> Type where
102 C_Str : C_Types String
103 C_Float : C_Types Double
105 C_MPtr : C_Types ManagedPtr
107 C_Any : C_Types (Raw a)
108 C_FnT : C_FnTypes t -> C_Types (CFnPtr t)
109 C_IntT : C_IntTypes i -> C_Types i
111 ||| A descriptor for the C FFI. See the constructors of `C_Types`
112 ||| and `C_IntTypes` for the concrete types that are available.
116 FFI_C = MkFFI C_Types String String
121This is the example of linking C code.
130 DEFAULT: mylib.o main.idr
131 idris main.idr -o executableFile
134 rm -f executableFile mylib.o main.ibc
139To call a foreign function, the ``foreign`` function is used. For
144 do_fopen : String -> String -> IO Ptr
146 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
148The ``foreign`` function takes an FFI description, a function name (the
149type is given by the ``ffi_fn`` field of ``FFI_C`` here), and a function
150type, which gives the expected types of the remaining arguments. Here,
151we're calling an external function ``fileOpen`` which takes, in the C, a
152``char*`` file name, a ``char*`` mode, and returns a file pointer. It is
153the job of the C back end to convert Idris ``String`` to C ``char*``
156The argument types and return type given here must be present in the
157``fn_types`` predicate of the ``FFI_C`` description for the foreign
160**Note** The arguments to ``foreign`` *must* be known at compile time,
161because the foreign calls are generated statically. The ``%inline``
162directive on a function can be used to give hints to help this, for
163example a shorthand for calling external JavaScript functions:
168 jscall : (fname : String) -> (ty : Type) ->
169 {auto fty : FTy FFI_JS [] ty} -> ty
170 jscall fname ty = foreign FFI_JS fname ty
174It is possible to pass an Idris function to a C function taking a function
175pointer by using ``CFnPtr`` in the function type. The Idris function is passed
176to ``MkCFnPtr`` in the arguments. The example below shows declaring the C standard
177library function ``qsort`` which takes a pointer to a comparison function.
181 myComparer : Ptr -> Ptr -> Int
184 qsort : Ptr -> Int -> Int -> IO ()
185 qsort data elems elsize = foreign FFI_C "qsort"
186 (Ptr -> Int -> Int -> CFnPtr (Ptr -> Ptr -> Int) -> IO ())
187 data elems elsize (MkCFnPtr myComparer)
189There are a few limitations to callbacks in the C FFI. The foreign function can't
190take the function to make a callback of as an argument. This will give a
195 -- This does not work
196 example : (Int -> ()) -> IO ()
197 example f = foreign FFI_C "callbacker" (CFnPtr (Int -> ()) -> IO ()) f
199Note that the function that is used as a callback can't be a closure, that is
200it can't be a partially applied function. This is because the mechanism used is
201unable to pass the closed-over values through C. If we want to pass Idris values
202to the callback we have to pass them through C explicitly. Non-primitive Idris
203values can be passed to C via the ``Raw`` type.
205The other big limitation is that it doesn't support IO functions. Use
206``unsafePerformIO`` to wrap them (i.e. to make an IO function usable as a callback, change the return type
207from IOr to r, and change the = do to = unsafePerformIO $ do).
209There are two special function names:
210``%wrapper`` returns the function pointer that wraps an Idris function. This
211is useful if the function pointer isn't taken by a C function directly but
212should be inserted into a data structure. A foreign declaration using
213``%wrapper`` must return ``IO Ptr``.
217 -- this returns the C function pointer to a qsort comparer
218 example_wrapper : IO Ptr
219 example_wrapper = foreign FFI_C "%wrapper" (CFnPtr (Ptr -> Ptr -> Int) -> IO Ptr)
220 (MkCFnPtr myComparer)
222``%dynamic`` calls a C function pointer with some arguments. This is useful if
223a C function returns or data structure contains a C function pointer, for example
224structs of function pointers are common in object-oriented C such as in COM or the
225Linux kernel. The function type contains an extra ``Ptr`` at the start for the
226function pointer. ``%dynamic`` can be seen as a pseudo-function that calls the
227function in the first argument, passing the remaining arguments to it.
231 -- we have a pointer to a function with the signature int f(int), call it
232 example_dynamic : Ptr -> Int -> IO Int
233 example_dynamic fn x = foreign FFI_C "%dynamic" (Ptr -> Int -> IO Int) fn x
235If the foreign name is prefixed by a ``&``, it is treated as a pointer to the
236global variable with the following name. The type must be just ``IO Ptr``.
240 -- access the global variable errno
242 errno = foreign FFI_C "&errno" (IO Ptr)
244If the foreign name is prefixed by a ``#``, the name is pasted in literally. This is
245useful to access constants that are preprocessor definitions (like ``INT_MAX``).
249 %include C "limits.h"
251 -- access the preprocessor definition INT_MAX
253 intMax = foreign FFI_C "#INT_MAX" (IO Int)
258For more complicated interactions with C (such as reading and setting fields
259of a C struct), there is a module CFFI available in the contrib package.
264Idris has two heaps where objects can be allocated:
266+--------------------------------------+---------------------------------------+
268+======================================+=======================================+
269| Cheney-collected | Mark-and-sweep-collected |
270+--------------------------------------+---------------------------------------+
271| Garbage collections touches only | Garbage collection has to traverse |
272| live objects. | all registered items. |
273+--------------------------------------+---------------------------------------+
274| Ideal for FP-style rapid allocation | Ideal for C-style allocation of a few |
275| of lots of small short-lived pieces | big buffers. |
276| of memory, such as data constructors.| |
277+--------------------------------------+---------------------------------------+
278| Finalizers are impossible to support | Items have finalizers that are called |
279| reasonably. | on deallocation. |
280+--------------------------------------+---------------------------------------+
281| Data is copied all the time (when | Copying does not happen. |
282| collecting garbage, modifying data, | |
283| registering managed pointers, etc.) | |
284+--------------------------------------+---------------------------------------+
285| Contains objects of various types. | Contains C heap items: ``(void *)`` |
286| | pointers with finalizers. A finalizer |
287| | is a routine that deallocates the |
288| | resources associated with the item. |
289+--------------------------------------+---------------------------------------+
290| Fixed set of object types. | The data pointer may point |
291| | to anything, as long as the finalizer |
292| | cleans up correctly. |
293+--------------------------------------+---------------------------------------+
294| Not suitable for C resources and | Suitable for C resources and arbitrary|
295| arbitrary pointers. | pointers. |
296+--------------------------------------+---------------------------------------+
297| Values form a compact memory block. | Items are kept in a linked list. |
298+--------------------------------------+---------------------------------------+
299| Any Idris value, most notably | Items represented by the |
300| ``ManagedPtr``. | Idris type ``CData``. |
301+--------------------------------------+---------------------------------------+
302| Data of ``ManagedPtr`` allocated | Data allocated in C, pointer copied |
303| in C, buffer then copied into the FP | into the C heap. |
305+--------------------------------------+---------------------------------------+
306| Allocation and reallocation not | Allocated and reallocate freely in C, |
307| possible from C code (without having | registering the allocated items |
308| a reference to the VM). Everything | in the FFI. |
309| is copied instead. | |
310+--------------------------------------+---------------------------------------+
312The FP heap is the primary heap. It may contain values of type ``CData``,
313which are references to items in the C heap. A C heap item contains
314a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item
315is no longer referenced from the FP heap, it is marked as unused and
316the next GC sweep will call its finalizer and deallocate it.
318There is no Idris interface for ``CData`` other than its type and FFI.
323* Although not enforced in code, ``CData`` is meant to be opaque
324 and non-RTS code (such as libraries or C bindings) should
325 access only its ``(void *)`` field called ``data``.
327* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)
328 and the memory it points to. However, keep in mind
329 that this must not break Idris's referential transparency.
331* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,
332 the resulting ``CData`` object *must* be returned from your
333 FFI function so that it is inserted in the C heap by the RTS.
334 Otherwise the memory will be leaked.
338 some_allocating_fun : Int -> IO CData
339 some_allocating_fun i = foreign FFI_C "some_allocating_fun" (Int -> IO CData) i
341 other_fun : CData -> Int -> IO Int
342 other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i
346 #include "idris_rts.h"
348 static void finalizer(void * data)
350 MyStruct * ptr = (MyStruct *) data;
351 free_something(ptr->something);
355 CData some_allocating_fun(int arg)
357 size_t size = sizeof(...);
358 void * data = (void *) malloc(size);
360 return cdata_manage(data, size, finalizer);
363 int other_fun(CData cd, int arg)
365 int result = foo(cd->data);
369The ``Raw`` type constructor allows you to access or return a runtime
370representation of the value. For instance, if you want to copy a string
371generated from C code into an Idris value, you may want to return a
372``Raw String``instead of a ``String`` and use ``MKSTR`` or ``MKSTRlen`` to
377 getString : () -> IO (Raw String)
378 getString () = foreign FFI_C "get_string" (IO (Raw String))
382 const VAL get_string ()
384 char * c_string = get_string_allocated_with_malloc()
385 const VAL idris_string = MKSTR(c_string);
393In order to write bindings to external libraries, the details of how
394``foreign`` works are unnecessary --- you simply need to know that
395``foreign`` takes an FFI descriptor, the function name, and its
396type. It is instructive to look a little deeper, however:
398The type of ``foreign`` is as follows:
402 foreign : (ffi : FFI)
403 -> (fname : ffi_fn f)
405 -> {auto fty : FTy ffi [] ty}
408The important argument here is the implicit ``fty``, which contains a
409proof (``FTy``) that the given type is valid according to the FFI
414 data FTy : FFI -> List Type -> Type -> Type where
415 FRet : ffi_types f t -> FTy f xs (IO' f t)
416 FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
418Notice that this uses the ``ffi_types`` field of the FFI descriptor
419--- these arguments to ``FRet`` and ``FFun`` give explicit proofs that
420the type is valid in this FFI. For example, the above ``do_fopen``
421builds the following implicit proof as the ``fty`` argument to
426 FFun C_Str (FFun C_Str (FRet C_Ptr))
428Compiling foreign calls
429=======================
431(This section assumes some knowledge of the Idris internals.)
433When writing a back end, we now need to know how to compile
434``foreign``. We'll skip the details here of how a ``foreign`` call
435reaches the intermediate representation (the IR), though you can look
436in ``IO.idr`` in the ``prelude`` package to see a bit more detail ---
437a ``foreign`` call is implemented by the primitive function
438``mkForeignPrim``. The important part of the IR as defined in
439``Lang.hs`` is the following constructor:
444 | LForeign FDesc -- Function descriptor
445 FDesc -- Return type descriptor
448So, a ``foreign`` call appears in the IR as the ``LForeign``
449constructor, which takes a function descriptor (of a type given by the
450``ffi_fn`` field in the FFI descriptor), a return type descriptor
451(given by an application of ``FTy``), and a list of arguments with
452type descriptors (also given by an application of ``FTy``).
454An ``FDesc`` describes an application of a name to some arguments, and
455is really just a simplified subset of an ``LExp``:
459 data FDesc = FCon Name
464There are corresponding structures in the lower level IRs, such as the
465defunctionalised, simplified and bytecode forms.
467Our ``do_fopen`` example above arrives in the ``LExp`` form as:
471 LForeign (FStr "fileOpen") (FCon (sUN "C_Ptr"))
472 [(FCon (sUN "C_Str"), f), (FCon (sUN "C_Str"), m)]
474(Assuming that ``f`` and ``m`` stand for the ``LExp`` representations
475of the arguments.) This information should be enough for any back end
476to marshal the arguments and return value appropriately.
480 When processing ``FDesc``, be aware that there may be implicit
481 arguments, which have not been erased. For example, ``C_IntT`` has
482 an implicit argument ``i``, so will appear in an ``FDesc`` as
483 something of the form ``FApp (sUN "C_IntT") [i, t]`` where ``i`` is
484 the implicit argument (which can be ignored) and ``t`` is the
485 descriptor of the integer type. See ``CodegenC.hs``, specifically
486 the function ``toFType``, to see how this works in practice.
488JavaScript FFI descriptor
489=========================
491The JavaScript FFI descriptor is a little more complex, because the
492JavaScript FFI supports marshalling functions. It is defined as
498 data JsFn t = MkJsFn t
500 data JS_IntTypes : Type -> Type where
501 JS_IntChar : JS_IntTypes Char
502 JS_IntNative : JS_IntTypes Int
504 data JS_FnTypes : Type -> Type where
505 JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
506 JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
507 JS_FnBase : JS_Types t -> JS_FnTypes t
509 data JS_Types : Type -> Type where
510 JS_Str : JS_Types String
511 JS_Float : JS_Types Double
512 JS_Ptr : JS_Types Ptr
513 JS_Unit : JS_Types ()
514 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
515 JS_IntT : JS_IntTypes i -> JS_Types i
517The reason for wrapping function types in a ``JsFn`` is to help the
518proof search when building ``FTy``. We hope to improve proof search
519eventually, but for the moment it works much more reliably if the
520indices are disjoint! An example of using this appears in `IdrisScript
521<https://github.com/idris-hackers/IdrisScript>`__ when setting
526 setTimeout : (() -> JS_IO ()) -> (millis : Int) -> JS_IO Timeout
527 setTimeout f millis = do
528 timeout <- jscall "setTimeout(%0, %1)"
529 (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
531 pure $ MkTimeout timeout
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list