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).

Installation

Requirements

• Stack:
• OCaml 4.07.01+flambda
• Opam

Clone this repository:

$ git clone --recurse-submodules https://github.com/ioanluca/real-world-idris.git
$ 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.

Usage

$ 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.

Examples

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"

Benchmarking

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

Todo

• 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

Contributing

Contributions are welcome!