Simple FFI in Idris
FFI Foreign Functions Inerface allows you to call a code written in one language from a code written in another language. In this post I will show you how to do that in dependently typed programming language called Idris. We will be able to call C code from Idris and vice versa.
First let’s create simple program in C which will allow us to calculate factorial (file
Header file is also required as it will provide a function declaration for our exposed factorial function (file
Now you should be able to compile it with GCC like this
$ gcc -c factorial.c
Once that done let’s look at Idris code which needs only two extra directives to make everything works
As you can see we define a function as usually with a special call to foreign and the rest is handled by the underlying runtime implementation.
Now you are able to either compile your code or call it directly from a REPL
$ idris ffi.idr -o ffi
For this example we are going to create Idris data type which is equivalent to the list of integers (file
nil : List Int
cons functions allowing to construct a list and helper
showList function which displays our list on a screen. As opposed to C header file which declares functions we need to have special export functions (
exportList from the above) which defines functions and types alongside their aliases as a return value. To proceed type
idris list.idr --interface -o list.o into a shell. This code will generate object file and a header which we are going to include into our C source code
C part is a bit trickier as we need to create an Idris virtual machine which will be running our functions and every function call also expects
vm as a first parameter. At the end we need to free resources, so there is a
close_vm call as well.
Finally back to our compilation command which is a bit complex this time
$ gcc idris_list.c list.o `idris $@ --include` `idris $@ --link` -o list
and if nothing goes wrong you should be able to run
Ok, at this point you should have an overall idea of how to do inter-language calls. This might be useful for creating language bindings for popular libraries in Idris (like this Qt binding for Haskell for example). So if you are interested in developing ecosystem for this amazing language here’s your next adventure. Happy coding!