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 instance 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
121To call a foreign function, the ``foreign`` function is used. For
126 do_fopen : String -> String -> IO Ptr
128 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
130The ``foreign`` function takes an FFI description, a function name (the
131type is given by the ``ffi_fn`` field of ``FFI_C`` here), and a function
132type, which gives the expected types of the remaining arguments. Here,
133we're calling an external function ``fileOpen`` which takes, in the C, a
134``char*`` file name, a ``char*`` mode, and returns a file pointer. It is
135the job of the C back end to convert Idris ``String`` to C ``char*``
138The argument types and return type given here must be present in the
139``fn_types`` predicate of the ``FFI_C`` description for the foreign
142**Note** The arguments to ``foreign`` *must* be known at compile time,
143because the foreign calls are generated statically. The ``%inline``
144directive on a function can be used to give hints to help this, for
145example a shorthand for calling external JavaScript functions:
150 jscall : (fname : String) -> (ty : Type) ->
151 {auto fty : FTy FFI_JS [] ty} -> ty
152 jscall fname ty = foreign FFI_JS fname ty
156It is possible to pass an Idris function to a C function taking a function
157pointer by using ``CFnPtr`` in the function type. The Idris function is passed
158to ``MkCFnPtr`` in the arguments. The example below shows declaring the C standard
159library function ``qsort`` which takes a pointer to a comparison function.
163 myComparer : Ptr -> Ptr -> Int
166 qsort : Ptr -> Int -> Int -> IO ()
167 test2 data elems elsize = foreign FFI_C "qsort"
168 (Ptr -> Int -> Int -> CFnPtr (Ptr -> Ptr -> Int) -> IO ())
169 data elems elsize (MkCFnPtr myComparer)
171There are a few limitations to callbacks in the C FFI. The foreign function can't
172take the function to make a callback of as an argument. This will give a
177 -- This does not work
178 example : (Int -> ()) -> IO ()
179 example f = foreign FFI_C "callbacker" (CFnPtr (Int -> ()) -> IO ()) f
181The other big limitation is that it doesn't support IO functions. Use
182``unsafePerformIO`` to wrap them (i.e. to make an IO function usable as a callback, change the return type
183from IOr to r, and change the = do to = unsafePerformIO $ do).
185There are two special function names:
186``%wrapper`` returns the function pointer that wraps an Idris function. This
187is useful if the function pointer isn't taken by a C function directly but
188should be inserted into a data structure. A foreign declaration using
189``%wrapper`` must return ``IO Ptr``.
193 -- this returns the C function pointer to a qsort comparer
194 example_wrapper : IO Ptr
195 example_wrapper = foreign FFI_C "%wrapper" (CFnPtr (Ptr -> Ptr -> Int) -> IO Ptr)
196 (MkCFnPtr myComparer)
198``%dynamic`` calls a C function pointer with some arguments. This is useful if
199a C function returns or data structure contains a C function pointer, for example
200structs of function pointers are common in object-oriented C such as in COM or the
201Linux kernel. The function type contains an extra ``Ptr`` at the start for the
202function pointer. ``%dynamic`` can be seen as a pseudo-function that calls the
203function in the first argument, passing the remaining arguments to it.
207 -- we have a pointer to a function with the signature int f(int), call it
208 example_dynamic : Ptr -> Int -> IO Int
209 example_dynamic fn x = foreign FFI_C "%dynamic" (Ptr -> Int -> IO Int) fn x
211If the foreign name is prefixed by a ``&``, it is treated as a pointer to the
212global variable with the following name. The type must be just ``IO Ptr``.
216 -- access the global variable errno
218 errno = foreign FFI_C "&errno" (IO Ptr)
220For more complicated interactions with C (such as reading and setting fields of a C struct), there is
221a module CFFI available in the contrib package.
226In order to write bindings to external libraries, the details of how
227``foreign`` works are unnecessary --- you simply need to know that
228``foreign`` takes an FFI descriptor, the function name, and its
229type. It is instructive to look a little deeper, however:
231The type of ``foreign`` is as follows:
235 foreign : (ffi : FFI)
236 -> (fname : ffi_fn f)
238 -> {auto fty : FTy ffi [] ty}
241The important argument here is the implicit ``fty``, which contains a
242proof (``FTy``) that the given type is valid according to the FFI
247 data FTy : FFI -> List Type -> Type -> Type where
248 FRet : ffi_types f t -> FTy f xs (IO' f t)
249 FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
251Notice that this uses the ``ffi_types`` field of the FFI descriptor
252--- these arguments to ``FRet`` and ``FFun`` give explicit proofs that
253the type is valid in this FFI. For example, the above ``do_fopen``
254builds the following implicit proof as the ``fty`` argument to
259 FFun C_Str (FFun C_Str (FRet C_Ptr))
261Compiling foreign calls
262=======================
264(This section assumes some knowledge of the Idris internals.)
266When writing a back end, we now need to know how to compile
267``foreign``. We'll skip the details here of how a ``foreign`` call
268reaches the intermediate representation (the IR), though you can look
269in ``IO.idr`` in the ``prelude`` package to see a bit more detail ---
270a ``foreign`` call is implemented by the primitive function
271``mkForeignPrim``. The important part of the IR as defined in
272``Lang.hs`` is the following constructor:
277 | LForeign FDesc -- Function descriptor
278 FDesc -- Return type descriptor
281So, a ``foreign`` call appears in the IR as the ``LForeign``
282constructor, which takes a function descriptor (of a type given by the
283``ffi_fn`` field in the FFI descriptor), a return type descriptor
284(given by an application of ``FTy``), and a list of arguments with
285type descriptors (also given by an application of ``FTy``).
287An ``FDesc`` describes an application of a name to some arguments, and
288is really just a simplified subset of an ``LExp``:
292 data FDesc = FCon Name
297There are corresponding structures in the lower level IRs, such as the
298defunctionalised, simplified and bytecode forms.
300Our ``do_fopen`` example above arrives in the ``LExp`` form as:
304 LForeign (FStr "fileOpen") (FCon (sUN "C_Ptr"))
305 [(FCon (sUN "C_Str"), f), (FCon (sUN "C_Str"), m)]
307(Assuming that ``f`` and ``m`` stand for the ``LExp`` representations
308of the arguments.) This information should be enough for any back end
309to marshal the arguments and return value appropriately.
313 When processing ``FDesc``, be aware that there may be implicit
314 arguments, which have not been erased. For example, ``C_IntT`` has
315 an implicit argument ``i``, so will appear in an ``FDesc`` as
316 something of the form ``FApp (sUN "C_IntT") [i, t]`` where ``i`` is
317 the implicit argument (which can be ignored) and ``t`` is the
318 descriptor of the integer type. See ``CodegenC.hs``, specifically
319 the function ``toFType``, to see how this works in practice.
321JavaScript FFI descriptor
322=========================
324The JavaScript FFI descriptor is a little more complex, because the
325JavaScript FFI supports marshalling functions. It is defined as
331 data JsFn t = MkJsFn t
333 data JS_IntTypes : Type -> Type where
334 JS_IntChar : JS_IntTypes Char
335 JS_IntNative : JS_IntTypes Int
337 data JS_FnTypes : Type -> Type where
338 JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
339 JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
340 JS_FnBase : JS_Types t -> JS_FnTypes t
342 data JS_Types : Type -> Type where
343 JS_Str : JS_Types String
344 JS_Float : JS_Types Float
345 JS_Ptr : JS_Types Ptr
346 JS_Unit : JS_Types ()
347 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
348 JS_IntT : JS_IntTypes i -> JS_Types i
350The reason for wrapping function types in a ``JsFn`` is to help the
351proof search when building ``FTy``. We hope to improve proof search
352eventually, but for the moment it works much more reliably if the
353indices are disjoint! An example of using this appears in `IdrisScript
354<https://github.com/idris-hackers/IdrisScript>`__ when setting
359 setTimeout : (() -> JS_IO ()) -> (millis : Int) -> JS_IO Timeout
360 setTimeout f millis = do
361 timeout <- jscall "setTimeout(%0, %1)"
362 (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
364 return $ 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