Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 15:20 - 15:45 at Pine - Session 4 Chair(s): Gabriel Scherer

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.

Thu 22 Aug

mlfamilyworkshop-2019-papers
15:20 - 16:30: ML 2019 - Session 4 at Pine
Chair(s): Gabriel SchererINRIA Saclay
mlfamilyworkshop-2019-papers15:20 - 15:45
Talk
Robert AtkeyUniversity of Strathclyde, Ioan LucaUniversity of Strathclyde
File Attached
mlfamilyworkshop-2019-papers15:45 - 16:10
Talk
File Attached