git.iko.soy/Idris-dev
on 8a3d348 help sign in
Idris-dev/docs/reference/ffi.rst
278 lines 9.6 kB history raw
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
20describes.
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:
30.. code-block:: idris
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:
38.. code-block:: idris
40 FFI_C : FFI
41 FFI_JS : FFI
43 IO : Type -> Type
44 IO a = IO' FFI_C a
46 JS_IO : Type -> Type
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:
53.. code-block:: idris
55 main : IO ()
56 main : JS_IO ()
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).
64FFI descriptors
65===============
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
69call:
71.. code-block:: idris
73 record FFI : Type where
74 MkFFI : (ffi_types : Type -> Type) ->
75 (ffi_fn : Type) -> FFI
77For C, this is:
79.. code-block:: idris
81 -- Supported C integer types
82 data C_IntTypes : Type -> Type where
83 C_IntChar : C_IntTypes Char
84 C_IntNative : C_IntTypes Int
85 ... -- more integer types
87 -- Supported C foreign types
88 data C_Types : Type -> Type where
89 C_Str : C_Types String
90 C_Float : C_Types Float
91 C_Ptr : C_Types Ptr
92 C_MPtr : C_Types ManagedPtr
93 C_Unit : C_Types ()
94 C_Any : C_Types (Raw a)
95 C_IntT : C_IntTypes i -> C_Types i
97 FFI_C : FFI
98 FFI_C = MkFFI C_Types
99 String -- the name of the C function
101Foreign calls
102=============
104To call a foreign function, the ``foreign`` function is used. For
105example:
107.. code-block:: idris
109 do_fopen : String -> String -> IO Ptr
110 do_fopen f m
111 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
113The ``foreign`` function takes an FFI description, a function name (the
114type is given by the ``ffi_fn`` field of ``FFI_C`` here), and a function
115type, which gives the expected types of the remaining arguments. Here,
116we're calling an external function ``fileOpen`` which takes, in the C, a
117``char*`` file name, a ``char*`` mode, and returns a file pointer. It is
118the job of the C back end to convert Idris ``String`` to C ``char*``
119and vice versa.
121The argument types and return type given here must be present in the
122``fn_types`` predicate of the ``FFI_C`` description for the foreign
123call to be valid.
125**Note** The arguments to ``foreign`` *must* be known at compile time,
126because the foreign calls are generated statically. The ``%inline``
127directive on a function can be used to give hints to help this, for
128example a shorthand for calling external JavaScript functions:
130.. code-block:: idris
132 %inline
133 jscall : (fname : String) -> (ty : Type) ->
134 {auto fty : FTy FFI_JS [] ty} -> ty
135 jscall fname ty = foreign FFI_JS fname ty
137FFI implementation
138------------------
140In order to write bindings to external libraries, the details of how
141``foreign`` works are unnecessary --- you simply need to know that
142``foreign`` takes an FFI descriptor, the function name, and its
143type. It is instructive to look a little deeper, however:
145The type of ``foreign`` is as follows:
147.. code-block:: idris
149 foreign : (ffi : FFI)
150 -> (fname : ffi_fn f)
151 -> (ty : Type)
152 -> {auto fty : FTy ffi [] ty}
153 -> ty
155The important argument here is the implicit ``fty``, which contains a
156proof (``FTy``) that the given type is valid according to the FFI
157description ``ffi``:
159.. code-block:: idris
161 data FTy : FFI -> List Type -> Type -> Type where
162 FRet : ffi_types f t -> FTy f xs (IO' f t)
163 FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
165Notice that this uses the ``ffi_types`` field of the FFI descriptor
166--- these arguments to ``FRet`` and ``FFun`` give explicit proofs that
167the type is valid in this FFI. For example, the above ``do_fopen``
168builds the following implicit proof as the ``fty`` argument to
169``foreign``:
171.. code-block:: idris
173 FFun C_Str (FFun C_Str (FRet C_Ptr))
175Compiling foreign calls
176=======================
178(This section assumes some knowledge of the Idris internals.)
180When writing a back end, we now need to know how to compile
181``foreign``. We'll skip the details here of how a ``foreign`` call
182reaches the intermediate representation (the IR), though you can look
183in ``IO.idr`` in the ``prelude`` package to see a bit more detail ---
184a ``foreign`` call is implemented by the primitive function
185``mkForeignPrim``. The important part of the IR as defined in
186``Lang.hs`` is the following constructor:
188.. code-block:: idris
190 data LExp = ...
191 | LForeign FDesc -- Function descriptor
192 FDesc -- Return type descriptor
193 [(FDesc, LExp)]
195So, a ``foreign`` call appears in the IR as the ``LForeign``
196constructor, which takes a function descriptor (of a type given by the
197``ffi_fn`` field in the FFI descriptor), a return type descriptor
198(given by an application of ``FTy``), and a list of arguments with
199type descriptors (also given by an application of ``FTy``).
201An ``FDesc`` describes an application of a name to some arguments, and
202is really just a simplified subset of an ``LExp``:
204.. code-block:: idris
206 data FDesc = FCon Name
207 | FStr String
208 | FUnknown
209 | FApp Name [FDesc]
211There are corresponding structures in the lower level IRs, such as the
212defunctionalised, simplified and bytecode forms.
214Our ``do_fopen`` example above arrives in the ``LExp`` form as:
216.. code-block:: idris
218 LForeign (FStr "fileOpen") (FCon (sUN "C_Ptr"))
219 [(FCon (sUN "C_Str"), f), (FCon (sUN "C_Str"), m)]
221(Assuming that ``f`` and ``m`` stand for the ``LExp`` representations
222of the arguments.) This information should be enough for any back end
223to marshal the arguments and return value appropriately.
225.. note::
227 When processing ``FDesc``, be aware that there may be implicit
228 arguments, which have not been erased. For example, ``C_IntT`` has
229 an implicit argument ``i``, so will appear in an ``FDesc`` as
230 something of the form ``FApp (sUN "C_IntT") [i, t]`` where ``i`` is
231 the implicit argument (which can be ignored) and ``t`` is the
232 descriptor of the integer type. See ``CodegenC.hs``, specifically
233 the function ``toFType``, to see how this works in practice.
235JavaScript FFI descriptor
236=========================
238The JavaScript FFI descriptor is a little more complex, because the
239JavaScript FFI supports marshalling functions. It is defined as
240follows:
242.. code-block:: idris
244 mutual
245 data JsFn t = MkJsFn t
247 data JS_IntTypes : Type -> Type where
248 JS_IntChar : JS_IntTypes Char
249 JS_IntNative : JS_IntTypes Int
251 data JS_FnTypes : Type -> Type where
252 JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
253 JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
254 JS_FnBase : JS_Types t -> JS_FnTypes t
256 data JS_Types : Type -> Type where
257 JS_Str : JS_Types String
258 JS_Float : JS_Types Float
259 JS_Ptr : JS_Types Ptr
260 JS_Unit : JS_Types ()
261 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
262 JS_IntT : JS_IntTypes i -> JS_Types i
264The reason for wrapping function types in a ``JsFn`` is to help the
265proof search when building ``FTy``. We hope to improve proof search
266eventually, but for the moment it works much more reliably if the
267indices are disjoint! An example of using this appears in `IdrisScript
268<https://github.com/idris-hackers/IdrisScript>`__ when setting
269timeouts:
271.. code-block:: idris
273 setTimeout : (() -> JS_IO ()) -> (millis : Int) -> JS_IO Timeout
274 setTimeout f millis = do
275 timeout <- jscall "setTimeout(%0, %1)"
276 (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
277 (MkJsFn f) millis
278 return $ MkTimeout timeout