Montag, 21. Januar 2013

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.

Freitag, 18. Januar 2013

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: