Code Generation Targets

Idris has been designed such that the compiler can generate code for different backends upon request. By default Idris generates a C backend when generating an executable. Included within the standard Idris installation are backends for Javascript and Node.js.

However, there are third-party code generators out there. Below we describe some of these backends and how you can use them when compiling your Idris code. If you want to write your own codegen for your language there is a stub project on GitHub that can help point you in the right direction.

Official Backends

C Language

The default target of Idris is C. In order to view the generated C code, compile via:

$ idris hello.idr -S -o hello.c

Javascript

To generate code that is tailored for running in the browser issue the following command:

$ idris --codegen javascript hello.idr -o hello.js

Idris can produce big chunks of JavaScript code (hello world weighs in at about 60 lines). However, the generated code can be minified using the closure-compiler from Google.

java -jar compiler.jar --compilation_level ADVANCED_OPTIMIZATIONS --js hello.js

Node.js

Generating code for NodeJS is slightly different. Idris outputs a JavaScript file that can be directly executed via node.

$ idris --codegen node hello.idr -o hello
$ ./hello
Hello world

Third Party

Note

These are third-party code generations and may have bit-rotted or do not work with current versions of Idris. Please speak to the project’s maintainers if there are any problems.

CIL (.NET, Mono, Unity)

idris --codegen cil Main.idr -o HelloWorld.exe \
  && mono HelloWorld.exe

The resulting assemblies can also be used with .NET or Unity.

Requires idris-cil.

Java

Available online

idris hello.idr --codegen java -o hello.jar

Note: The resulting .jar is automatically prefixed by a header including an .sh script to allow executing it directly.

Malfunction

Available online

WebAssembly

Available online