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