1New Foreign Function Interface
2==============================
4.. sectionauthor:: Edwin Brady
6Ever since Idris has had multiple backends compiling to different target
7languages on potentially different platforms, we have had the problem
8that the foreign function interface (FFI) was written under the
9assumption of compiling to C. As a result, it has been hard to write
10generic code for multiple targets, or even to be sure that if code
11compiles that it will run on the expected target.
13As of 0.9.17, Idris will have a new foreign function interface (FFI)
14which is aware of multiple targets. Users who are working with the
15default code generator can happily continue writing programs as before
16with no changes, but if you are writing bindings for an external
17library, writing a back end, or working with a non-C back end, there are
18some things you will need to be aware of, which this page describes.
20The ``IO'`` monad, and ``main``
21-------------------------------
23The ``IO`` monad exists as before, but is now specific to the C backend
24(or, more precisely, any backend whose foreign function calls are
25compatible with C.) Additionally, there is now an ``IO'`` monad, which
26is parameterised over a FFI descriptor:
30 data IO' : (lang : FFI) -> Type -> Type
32The Prelude defines two FFI descriptors which are imported
33automatically, for C and JavaScript/Node, and defines ``IO`` to use the
34C FFI and ``JS_IO`` to use the JavaScript FFI:
45 JS_IO a = IO' FFI_JS a
47As before, the entry point to an Idris program is ``main``, but the type
48of ``main`` can now be any instance of ``IO'``, e.g. the following are
56The FFI descriptor includes details about which types can be marshalled
57between the foreign language and Idris, and the "target" of a foreign
58function call (typically just a String representation of the function's
59name, but potentially something more complicated such as an external
60library file or even a URL).
65An FFI descriptor is a record containing a predicate which holds when a
66type can be marshalled, and the type of the target of a foreign call:
70 record FFI : Type where
71 MkFFI : (ffi_types : Type -> Type) ->
72 (ffi_fn : Type) -> FFI
78 -- Supported C integer types
79 data C_IntTypes : Type -> Type where
80 C_IntChar : C_IntTypes Char
81 C_IntNative : C_IntTypes Int
82 ... -- more integer types
84 -- Supported C foreign types
85 data C_Types : Type -> Type where
86 C_Str : C_Types String
87 C_Float : C_Types Float
89 C_MPtr : C_Types ManagedPtr
91 C_Any : C_Types (Raw a)
92 C_IntT : C_IntTypes i -> C_Types i
96 String -- the name of the C function
101To call a foreign function, the ``foreign`` function is used. For
106 do_fopen : String -> String -> IO Ptr
108 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
110The ``foreign`` function takes an FFI description, a function name (the
111type is given by the ``ffi_fn`` field of ``FFI_C`` here), and a function
112type, which gives the expected types of the remaining arguments. Here,
113we're calling an external function ``fileOpen`` which takes, in the C, a
114``char*`` file name, a ``char*`` mode, and returns a file pointer. It is
115the job of the C back end to convert Idris ``String``\ s to C ``char*``
118The argument types and return type given here must be present in the
119``fn_types`` predicate of the ``FFI_C`` description for the foreign call
122**Note** The arguments to ``foreign`` *must* be known at compile time,
123because the foreign calls are generated statically. The ``%inline``
124directive on a function can be used to give hints to help this, for
125example a shorthand for calling external JavaScript functions:
130 jscall : (fname : String) -> (ty : Type) ->
131 {auto fty : FTy FFI_JS [] ty} -> ty
132 jscall fname ty = foreign FFI_JS fname ty
137In order to write bindings to external libraries, the details of how
138``foreign`` works are unnecessary --- you simply need to know that
139``foreign`` takes an FFI descriptor, the function name, and its type. It
140is instructive to look a little deeper, however:
142The type of ``foreign`` is as follows:
146 foreign : (ffi : FFI) -> (fname : ffi_fn f) -> (ty : Type) -> {auto fty : FTy ffi [] ty} -> ty
148The important argument here is the implicit ``fty``, which contains a
149proof (``FTy``) that the given type is valid according to the FFI
154 data FTy : FFI -> List Type -> Type -> Type where
155 FRet : ffi_types f t -> FTy f xs (IO' f t)
156 FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
158Notice that this uses the ``ffi_types`` field of the FFI descriptor ---
159these arguments to ``FRet`` and ``FFun`` give explicit proofs that the
160type is valid in this FFI. For example, the above ``do_fopen`` builds
161the following implicit proof as the ``fty`` argument to ``foreign``:
165 FFun C_Str (FFun C_Str (FRet C_Ptr))
167Compiling foreign calls
168-----------------------
170(This section assumes some knowledge of the Idris internals.)
172When writing a back end, we now need to know how to compile ``foreign``.
173We'll skip the details here of how a ``foreign`` call reaches the
174intermediate representation (the IR), though you can look in ``IO.idr``
175in the ``prelude`` package to see a bit more detail --- a ``foreign``
176call is implemented by the primitive function ``mkForeignPrim``. The
177important part of the IR as defined in ``Lang.hs`` is the following
183 | LForeign FDesc -- Function descriptor
184 FDesc -- Return type descriptor
187So, a ``foreign`` call appears in the IR as the ``LForeign``
188constructor, which takes a function descriptor (of a type given by the
189``ffi_fn`` field in the FFI descriptor), a return type descriptor (given
190by an application of ``FTy``), and a list of arguments with type
191descriptors (also given by an application of ``FTy``).
193An ``FDesc`` describes an application of a name to some arguments, and
194is really just a simplified subset of an ``LExp``:
198 data FDesc = FCon Name
203There are corresponding structures in the lower level IRs, such as the
204defunctionalised, simplified and bytecode forms.
206Our ``do_fopen`` example above arrives in the ``LExp`` form as:
210 LForeign (FStr "fileOpen") (FCon (sUN "C_Ptr"))
211 [(FCon (sUN "C_Str"), f), (FCon (sUN "C_Str"), m)]
213(Assuming that ``f`` and ``m`` stand for the ``LExp`` representations of
214the arguments.) This information should be enough for any back end to
215marshal the arguments and return value appropriately.
219 When processing ``FDesc``, be aware that there may be implicit
220 arguments, which have not been erased. For example, ``C_IntT`` has
221 an implicit argument ``i``, so will appear in an ``FDesc`` as
222 something of the form ``FApp (sUN "C_IntT") [i, t]`` where ``i`` is
223 the implicit argument (which can be ignored) and ``t`` is the
224 descriptor of the integer type. See ``CodegenC.hs``, specifically
225 the function ``toFType``, to see how this works in practice.
227JavaScript FFI descriptor
228~~~~~~~~~~~~~~~~~~~~~~~~~
230The JavaScript FFI descriptor is a little more complex, because the
231JavaScript FFI supports marshalling functions. It is defined as follows:
236 data JsFn t = MkJsFn t
238 data JS_IntTypes : Type -> Type where
239 JS_IntChar : JS_IntTypes Char
240 JS_IntNative : JS_IntTypes Int
242 data JS_FnTypes : Type -> Type where
243 JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
244 JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
245 JS_FnBase : JS_Types t -> JS_FnTypes t
247 data JS_Types : Type -> Type where
248 JS_Str : JS_Types String
249 JS_Float : JS_Types Float
250 JS_Ptr : JS_Types Ptr
251 JS_Unit : JS_Types ()
252 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
253 JS_IntT : JS_IntTypes i -> JS_Types i
255The reason for wrapping function types in a ``JsFn`` is to help the
256proof search when building ``FTy``. We hope to improve proof search
257eventually, but for the moment it works much more reliably if the
258indices are disjoint! An example of using this appears in
259`IdrisScript <https://github.com/idris-hackers/IdrisScript>`__ when
264 setTimeout : (() -> JS_IO ()) -> (millis : Int) -> JS_IO Timeout
265 setTimeout f millis = do
266 timeout <- jscall "setTimeout(%0, %1)"
267 (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
269 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