git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/docs/reference/ffi.rst
277 lines 9.5 kB history raw
1New Foreign Function Interface
2==============================
4.. sectionauthor:: Edwin Brady
6Ever since Idris has had multiple backends compiling to different
7target languages on potentially different platforms, we have had the
8problem that the foreign function interface (FFI) was written under
9the assumption of compiling to C. As a result, it has been hard to
10write generic code for multiple targets, or even to be sure that if
11code compiles 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
18are some things you will need to be aware of, which this page
19describes.
21The ``IO'`` monad, and ``main``
22-------------------------------
24The ``IO`` monad exists as before, but is now specific to the C
25backend (or, more precisely, any backend whose foreign function calls
26are compatible with C.) Additionally, there is now an ``IO'`` monad,
27which is parameterised over a FFI descriptor:
29.. code-block:: idris
31 data IO' : (lang : FFI) -> Type -> Type
33The Prelude defines two FFI descriptors which are imported
34automatically, for C and JavaScript/Node, and defines ``IO`` to use
35the C FFI and ``JS_IO`` to use the JavaScript FFI:
37.. code-block:: idris
39 FFI_C : FFI
40 FFI_JS : FFI
42 IO : Type -> Type
43 IO a = IO' FFI_C a
45 JS_IO : Type -> Type
46 JS_IO a = IO' FFI_JS a
48As before, the entry point to an Idris program is ``main``, but the
49type of ``main`` can now be any instance of ``IO'``, e.g. the
50following are both valid:
52.. code-block:: idris
54 main : IO ()
55 main : JS_IO ()
57The FFI descriptor includes details about which types can be
58marshalled between the foreign language and Idris, and the "target" of
59a foreign function call (typically just a String representation of the
60function's name, but potentially something more complicated such as an
61external library file or even a URL).
63FFI descriptors
64---------------
66An FFI descriptor is a record containing a predicate which holds when
67a type can be marshalled, and the type of the target of a foreign
68call:
70.. code-block:: idris
72 record FFI : Type where
73 MkFFI : (ffi_types : Type -> Type) ->
74 (ffi_fn : Type) -> FFI
76For C, this is:
78.. code-block:: idris
80 -- Supported C integer types
81 data C_IntTypes : Type -> Type where
82 C_IntChar : C_IntTypes Char
83 C_IntNative : C_IntTypes Int
84 ... -- more integer types
86 -- Supported C foreign types
87 data C_Types : Type -> Type where
88 C_Str : C_Types String
89 C_Float : C_Types Float
90 C_Ptr : C_Types Ptr
91 C_MPtr : C_Types ManagedPtr
92 C_Unit : C_Types ()
93 C_Any : C_Types (Raw a)
94 C_IntT : C_IntTypes i -> C_Types i
96 FFI_C : FFI
97 FFI_C = MkFFI C_Types
98 String -- the name of the C function
100Foreign calls
101-------------
103To call a foreign function, the ``foreign`` function is used. For
104example:
106.. code-block:: idris
108 do_fopen : String -> String -> IO Ptr
109 do_fopen f m
110 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
112The ``foreign`` function takes an FFI description, a function name (the
113type is given by the ``ffi_fn`` field of ``FFI_C`` here), and a function
114type, which gives the expected types of the remaining arguments. Here,
115we're calling an external function ``fileOpen`` which takes, in the C, a
116``char*`` file name, a ``char*`` mode, and returns a file pointer. It is
117the job of the C back end to convert Idris ``String`` to C ``char*``
118and vice versa.
120The argument types and return type given here must be present in the
121``fn_types`` predicate of the ``FFI_C`` description for the foreign
122call to be valid.
124**Note** The arguments to ``foreign`` *must* be known at compile time,
125because the foreign calls are generated statically. The ``%inline``
126directive on a function can be used to give hints to help this, for
127example a shorthand for calling external JavaScript functions:
129.. code-block:: idris
131 %inline
132 jscall : (fname : String) -> (ty : Type) ->
133 {auto fty : FTy FFI_JS [] ty} -> ty
134 jscall fname ty = foreign FFI_JS fname ty
136FFI implementation
137~~~~~~~~~~~~~~~~~~
139In order to write bindings to external libraries, the details of how
140``foreign`` works are unnecessary --- you simply need to know that
141``foreign`` takes an FFI descriptor, the function name, and its
142type. It is instructive to look a little deeper, however:
144The type of ``foreign`` is as follows:
146.. code-block:: idris
148 foreign : (ffi : FFI)
149 -> (fname : ffi_fn f)
150 -> (ty : Type)
151 -> {auto fty : FTy ffi [] ty}
152 -> ty
154The important argument here is the implicit ``fty``, which contains a
155proof (``FTy``) that the given type is valid according to the FFI
156description ``ffi``:
158.. code-block:: idris
160 data FTy : FFI -> List Type -> Type -> Type where
161 FRet : ffi_types f t -> FTy f xs (IO' f t)
162 FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
164Notice that this uses the ``ffi_types`` field of the FFI descriptor
165--- these arguments to ``FRet`` and ``FFun`` give explicit proofs that
166the type is valid in this FFI. For example, the above ``do_fopen``
167builds the following implicit proof as the ``fty`` argument to
168``foreign``:
170.. code-block:: idris
172 FFun C_Str (FFun C_Str (FRet C_Ptr))
174Compiling foreign calls
175-----------------------
177(This section assumes some knowledge of the Idris internals.)
179When writing a back end, we now need to know how to compile
180``foreign``. We'll skip the details here of how a ``foreign`` call
181reaches the intermediate representation (the IR), though you can look
182in ``IO.idr`` in the ``prelude`` package to see a bit more detail ---
183a ``foreign`` call is implemented by the primitive function
184``mkForeignPrim``. The important part of the IR as defined in
185``Lang.hs`` is the following constructor:
187.. code-block:: idris
189 data LExp = ...
190 | LForeign FDesc -- Function descriptor
191 FDesc -- Return type descriptor
192 [(FDesc, LExp)]
194So, a ``foreign`` call appears in the IR as the ``LForeign``
195constructor, which takes a function descriptor (of a type given by the
196``ffi_fn`` field in the FFI descriptor), a return type descriptor
197(given by an application of ``FTy``), and a list of arguments with
198type descriptors (also given by an application of ``FTy``).
200An ``FDesc`` describes an application of a name to some arguments, and
201is really just a simplified subset of an ``LExp``:
203.. code-block:: idris
205 data FDesc = FCon Name
206 | FStr String
207 | FUnknown
208 | FApp Name [FDesc]
210There are corresponding structures in the lower level IRs, such as the
211defunctionalised, simplified and bytecode forms.
213Our ``do_fopen`` example above arrives in the ``LExp`` form as:
215.. code-block:: idris
217 LForeign (FStr "fileOpen") (FCon (sUN "C_Ptr"))
218 [(FCon (sUN "C_Str"), f), (FCon (sUN "C_Str"), m)]
220(Assuming that ``f`` and ``m`` stand for the ``LExp`` representations
221of the arguments.) This information should be enough for any back end
222to marshal the arguments and return value appropriately.
224.. note::
226 When processing ``FDesc``, be aware that there may be implicit
227 arguments, which have not been erased. For example, ``C_IntT`` has
228 an implicit argument ``i``, so will appear in an ``FDesc`` as
229 something of the form ``FApp (sUN "C_IntT") [i, t]`` where ``i`` is
230 the implicit argument (which can be ignored) and ``t`` is the
231 descriptor of the integer type. See ``CodegenC.hs``, specifically
232 the function ``toFType``, to see how this works in practice.
234JavaScript FFI descriptor
235~~~~~~~~~~~~~~~~~~~~~~~~~
237The JavaScript FFI descriptor is a little more complex, because the
238JavaScript FFI supports marshalling functions. It is defined as
239follows:
241.. code-block:: idris
243 mutual
244 data JsFn t = MkJsFn t
246 data JS_IntTypes : Type -> Type where
247 JS_IntChar : JS_IntTypes Char
248 JS_IntNative : JS_IntTypes Int
250 data JS_FnTypes : Type -> Type where
251 JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
252 JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
253 JS_FnBase : JS_Types t -> JS_FnTypes t
255 data JS_Types : Type -> Type where
256 JS_Str : JS_Types String
257 JS_Float : JS_Types Float
258 JS_Ptr : JS_Types Ptr
259 JS_Unit : JS_Types ()
260 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
261 JS_IntT : JS_IntTypes i -> JS_Types i
263The reason for wrapping function types in a ``JsFn`` is to help the
264proof search when building ``FTy``. We hope to improve proof search
265eventually, but for the moment it works much more reliably if the
266indices are disjoint! An example of using this appears in `IdrisScript
267<https://github.com/idris-hackers/IdrisScript>`__ when setting
268timeouts:
270.. code-block:: idris
272 setTimeout : (() -> JS_IO ()) -> (millis : Int) -> JS_IO Timeout
273 setTimeout f millis = do
274 timeout <- jscall "setTimeout(%0, %1)"
275 (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
276 (MkJsFn f) millis
277 return $ MkTimeout timeout