Awesome Open Source
Awesome Open Source

Real World Idris

This is an experimental code generation backend for Idris that compiles it to a slightly modified version of Malfunction that has basic support for accessing identifiers outside the OCaml standard library.

This project also represents work in progress towards allowing Idris and OCaml to interoperate by implementing a ''Foreign Function Interface'' between the two languages using Idris' New FFI (described in Edwin Brady's paper and documented here).



Clone this repository:

$ git clone --recurse-submodules
$ cd real-world-idris/

Using Stack

$ stack build 

or, if you want to install the binaries globally:

$ stack install 
$ stack install idris 

All idris commands can be executed in the Stack sandbox by prepending them with stack exec --

Install Malfunction using Opam

In the root of the repository:

$ cd malfunction/
$ opam install .

Install the ocaml Idris package

In the root of the repository:

$ cd lib/
$ idris --install ocaml.ipkg

This needs to be used in Idris programs to access the FFI to OCaml.

Install the idrisobj OCaml package

In the root of the repository:

$ cd rts/
$ opam install .  

This is a runtime support library. It is a wrapper around the OCaml Obj module. The plan is to get rid of it and implement the required functions from Obj using Idris primitives.


$ idris Source.idr --codegen malfunction -p ocaml --cg-opt '-op ocamllib1 -op ocamllib2' -o a.out
$ ./a.out

-op is short for --ocamlpackage

Alternatively, %lib malfunction "ocamllib" can be used in an Idris file to link an OCaml library.


Some test programs can be found in test-idris.

To compile the graphics example:

$ cd test-idris/
$ cd graphics/
$ idris IdrCamlGrphics.idr --codegen malfunction -p ocaml --cg-opt '-op graphics' -o CamlGraphics.out
$ ./CamlGraphics.out

Note that the above example is linking the OCaml graphics module using the --cg-opt '-op graphics' flags.

Alternatively, graphics could also be linked by having the following line in IdrCamlGraphics.idr:

%lib malfunction "graphics"


Some example programs can be found in benchmark.

It seems to go pretty fast compared to the default C backend:

$ idris pythag.idr -o pythag-idris
$ idris pythag.idr --codegen malfunction -o pythag-malfunction
$ time ./pythag-idris  > /dev/null
real    0m4.548s
user    0m4.528s
sys     0m0.016s
$ time ./pythag-malfunction  > /dev/null
real    0m0.654s
user    0m0.652s
sys     0m0.000s

Tested on:

  • Ubuntu 16.04.4 LTS 64-bit
  • Intel® Core™ i5-2500 CPU @ 3.30GHz × 4
  • 8 GB RAM
  • Idris 1.2.0
  • Malfunction v0.2.1
  • OCaml 4.05.0+flambda


  • [ ] unicode, cannot just show KStrs, ocaml 8bit, overflow safety?
  • [ ] implement all primitives
  • [ ] use ocaml gc optimizations through env vars
  • [ ] tail calls
  • [ ] squeeze multiple lets together? let x = let y = 3 in
  • [ ] squeeze multiple lambdas together?
  • [ ] --interface flag?
  • [ ] dead code elimination (extra care with inlined definitions)
  • [ ] maybe get lang decls without liftings (if possible)
  • [ ] use state with a record for code generation monad?
  • [ ] use writerT and ReaderT instead of the Translate monad?
  • [ ] polymorphism (at the moment it is not possible to export polymorphic functions from Idris)
  • [ ] ADTs (separate from Idris' ADTs?)
  • [ ] User friendly modules (no way to name definitions right now)
  • [ ] Generating Idris type definitions from .cmi files
  • [ ] this Todo list


Contributions are welcome!

Related Awesome Lists
Top Programming Languages

Get A Weekly Email With Trending Projects For These Topics
No Spam. Unsubscribe easily at any time.
Tex (20,993
Compiler (15,733
Definition (7,851
Ocaml (6,955
Monad (1,939
Haskell Library (419
Idris (354
Dependent Types (236
Compiler Backend (16
Idris Ecosystem (12
Foreign Function Interface (3