Idris is a strict functional language with dependent types intended for practical use. Unfortunately, due to the relatively small size of the Idris user community, the ecosystem of available libraries for practical programming is limited. To remedy this, we have constructed a Foreign Function Interface (FFI) for Idris to call OCaml libraries. We have extended Dolan’s backend for the Idris compiler that generates Malfunction (a concrete syntax for the OCaml compiler’s Lambda intermediate language) with the ability to call arbitrary OCaml libraries. Using this facility, we have been able to call higher order functions in OCaml’s List library, use the Cohttp library to make a web server with the callback function written in Idris using the Lwt library, and to construct a simple Mirage unikernel written in Idris. In the latter case, we needed to export an implementation of an OCaml functor from Idris to fit with Mirage’s functorised design.

In the talk, we will report on and demo the modifications we have made to Dolan’s Malfunction backend to make it more efficient, and the design decisions we have taken in exposing parts of the complex OCaml type system in Idris. Idris’s dependent types offer us an expressive language for describing types themselves. However obstacles remain, including ergonomic expression of module types and type safe representation of polymorphic functions.