Shrinking Idris JavaScript with Closure

Compiling Idris to JavaScript can result in some pretty large files. In fact, small Idris programs can become so large that one might consider to fall back to JavaScript because it's just not worth it.

Let's take a look at a very simple example:

main : IO ()
main = do
  print l
where
  l : List Nat
  l = [1,2,3,4,5]

Let's compile this program and take a look at the size of the generated JavaScript.

raichoo@lain tmp» ls -lh test1.js
-rw-r--r-- 1 raichoo users 35K Feb 13 17:40 test1.js

35K of code is actually quite a lot for such a small program, but let's take into account that the file contains the whole runtime plus all needed parts of the standard library.

However, it gets even worse. The above program can be written in a different way. Let's give it a try.

module Main

main : IO ()
main = do
  print l
where
  l : List Nat
  l = [1..5]

Just a small change. Instead of writing down the whole List we are using a range. Now let's take a look at the output.

raichoo@lain tmp» ls -lh test2.js
-rw-r--r-- 1 raichoo users 99K Feb 13 17:45 test2.js

Yikes, 99K! How did that happen?

Ranges are not built in, they are just a syntax extension that has been defined in the standard library and it uses a couple of functions to do what it does. We are now pulling in even more of the standard library.

Anyway, a simple change and the code grows by a factor of almost 3. Granted, there is an upper bound to the amount of code we can pull in from the library, but that's not very comforting.

Is there something we can do about this?

Yes. The Google Closure compiler can do a whole lot of optimizations on JavaScript. Apart from the usual minifying it also can do inlining and dead code elimination.

Running Closure on our JavaScript files yields the following results:

raichoo@lain tmp» closure test1.js > test1-cl.js
raichoo@lain tmp» closure test2.js > test2-cl.js
raichoo@lain tmp» ls -lh test?-cl.js
-rw-r--r-- 1 raichoo users 20K Feb 13 18:12 test1-cl.js
-rw-r--r-- 1 raichoo users 63K Feb 13 18:13 test2-cl.js

That's smaller, but we can do even better. Idris targets Closure's advanced optimizations which can be enabled with the --compilation_level=ADVANCED_OPTIMIZATIONS flag (e.g. closure --compilation_level=ADVANCED_OPTIMIZATIONS). We don't need to take care of the Closure Guidelines ourselves, Idris does that for us.

Here's the result:

raichoo@lain tmp» ls -lh test?-cla.js
-rw-r--r-- 1 raichoo users 7.9K Feb 13 18:18 test1-cla.js
-rw-r--r-- 1 raichoo users  34K Feb 13 18:18 test2-cla.js

Now that's A LOT better. While Closure cannot get rid of the additional library code, it can eliminate code from Idris' runtime (we don't need big integers in this example, therefore Closure just get's rid of the code). Names get compressed and inlining takes place, etc etc.

I hope this shows that's Idris can create reasonably sized JavaScript files with a little help from it's friends.

Have fun with that!