Moving to raichoo.github.io

Hi, I've decided to move this blog to raichoo.github.io. Cya there!

Calling Idris from Javascript and vice-versa.

Until now the JavaScript backend for Idris has been a nice little gimmick to play around with, but when it comes to writing real applications it's pretty limited.
The limitations originates from the way how the FFI interacts with JavaScript. Until now it was not possible to call Idris code from within JavaScript which is essential when you want to register callbacks. In this blogpost I present my current work on the Idris FFI and JavaScript backend which enables this functionality. (Until these features have been merged into master you can track the development here)

Let's write a very simple piece of code that just changes a text label when it gets
clicked.

To do this we will need to define our onclick function. It'll look like this:

setOnClick : HTMLElement -> (() -> IO ()) -> IO ()
setOnClick (Elem p) f =
  mkForeign (FFun ".onclick=" [FPtr, FFunction FUnit (FAny (IO ()))] FUnit) p f

Let's break down what happens here. We are defining a function that takes an HTMLElement and a function that performs a side effect that should get executed whenever we click on the element. I'm using the FPtr type to represent a element. The name of the function tells the FFI that "onclick" is a field of an element. Whenever a name starts with a dot the FFI concludes that the first argument has to be an object and the name of the function is one of its fields. When the name ends with an equals sign it concludes that we are dealing with an assignment. In my previous blogposts I'm explaning how these mechanisms are used.
The second argument of our onclick function is of type "FFunction" takes an FUnit and returns a FAny (IO ()). mkForeign translates this into a function of type () -> IO (). For more information about the Idris FFI take a look at the tutorial. I've got a little bit of code on my gist that shows the FFI in action.

Have fun with calling functions back and forth :3

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!

Idris to JavaScript: Playing with the FFI

Until now the FFI for the JavaScript backend for Idris is quite primitive and somehow I'd like to keep it that way since I don't want to make invasive changes to the language just because of a different target. Therefore a started a little experiment to see how far one can get with the current FFI.
In JavaScript can have fields of objects, methods, functions, arrays etc etc. and we need to cover all these cases. Let's start with a little case study. We want to manipulate the DOM. Here is a little HTML snippet to begin with:

<html>
  <head>
  </head>
  <body>
    <div id="test">Foobar</div>
    <script src="test.js"></script>
  </body>
</html>

Now we want to replace the text of the Node with the id test

module Main

data HTMLElement : Type where
  Elem : Ptr -> HTMLElement

data NodeList : Type where
  Nodes : Ptr -> NodeList

query : String -> IO NodeList
query q = do
  e <- mkForeign (FFun "document.querySelectorAll" [FString] FPtr) q
  return (Nodes e)

item : NodeList -> Int -> IO HTMLElement
item (Nodes p) i = do
  i <- mkForeign (FFun ".item" [FPtr, FInt] FPtr) p i
  return (Elem i)

getId : HTMLElement -> IO String
getId (Elem p) = mkForeign (FFun ".id" [FPtr] FString) p

setText : HTMLElement -> String -> IO ()
setText (Elem p) s =
  mkForeign (FFun ".textContent=" [FPtr, FString] FUnit) p s

main : IO ()
main = do
  e <- query "#test"
  i <- item e 0
  s <- getId i
  setText i (s ++ ": SUPERFOO!!!")

In this example I'm using the Ptr type for raw JavaScript values and wrap them in ADTs. The interesting part is in the definition of the foreign functions. Functions starting with "." are methods or fields, that means that the first argument of the function is handled as and object and the function call gets translated into a method or field name. Functions ending with "=" are turned into assignments

Another thing we have to consider is that sometimes we want to refer to a method with no arguments, therefore we have to distinguish them from reading a field. In our example we read the value of the field id. If we wanted to turn that into a method call we need to declare it like this:

mkForeign (FFun ".id" [FPtr, FUnit] FString) p ()

We simply add an argument of type FUnit to the argument list and apply ().
Operations on arrays are declared like this:

mkForeign (FFun ".id[]" [FPtr, FInt] FString)
mkForeign (FFun ".id[]=" [FPtr, FInt, FString] FString)

The second argument is treated as an index
Working with the FFI is still dangerous, I'm currently unaware of a different way to do this without changing Idris' FFI which is something I don't want to. Another thing I don't want to do is making the FFI overly complex, it should be very low level and provide the basic building blocks for interacting with JavaScript. Anyway, patches are welcome ^^
One thing that might be worth considering is a way to declare safe foreign calls that do not need to be wrapped in IO.

Towards dependently typed webprogramming with Idris

JavaScript pretty much has become the lingua franka of the web. It runs in the browser, and since nodejs it's also possible to write server applications. However, it lacks a powerful type-system, and type-systems are something a lot of us have come to love. Anyway, this is not the time for the usual "dynamic vs. static" and "weak vs. strong typing" blog post. Today I want to write about a project I've started working on which brings dependent types to the JavaScript ecosystem meaning a JavaScript backend for the Idris compiler.
The foundation of this effort, the programming language Idris by Edwin Brady. Idris is basically the answer to the question: "What would Haskell look like if it had full dependent types?" It has strict semantics but also offers annotations for non-strict evaluation. If you want to know more about Idris can highly recommend the tutorial. Sadly there is not a lot of material out there to learn about programming with dependent types but I will link some resources in this blog post.
The backend itself compiles a large set of the language into a self contained Javascript file and offers a simple FFI to communicate with other libraries. It's still every experimental and I would not recommend to use it in your dayjob. However, if you feel like it feel free to contribute libraries and patches to complete the experience and transform Idris into a suitable language for web programming :)

How to use it:
Let's write a little Idris program and compile it to JavaScript:

module Main

product : List Integer -> Integer
product = foldl (*) 1

fac : Integer -> Integer
fac n = product [1..n]

main : IO ()
main = print (fac 300)

and compile it

> idris --target javascript test.idr -o test.js

and run it

> node test.js
… long output is long …

As you can see, the backend also supports big integers. The generated file is completely self contained including code from the standard library like typeclasses etc. (not everything but the code you need).
Now lets use the FFI to call into JavaScript land!

module Main

product : List Integer -> Integer
product = foldl (*) 1

fac : Integer -> Integer
fac n = product [1..n]

alert : String -> IO ()                                     
alert s = mkForeign (FFun "alert" [FString] FUnit) s

main : IO ()
main = alert $ show (fac 300)

Compile and run it in a browser of your choice ^^
This is just a little fraction of what you can do with the backend. Currently there is no support for types like Word8 and Word16 because it would not really make sense in a JavaScript context. There is also no support for filesystem operations. The code that gets generated is still rather large but with the google closure compiler you can reduce the size by a factor of 2 (advanced compilation is not supported at the moment).


References:

• Certified Programming With Dependent Types
• Talk by Andreas Bogk at Chaos Communication Camp 2011
• Agda Wiki