Javascript Notes

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

$ idris --codegen javascript hello.idr -o hello.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

IDRIS can produce very big chunks of JavaScript code (hello world weighs in at 1500 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