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:





Kommentare:

Anonym hat gesagt…

Hi. Supercool!

Two questions:
1. which "large set of the language" is it? (Any place to read about that?)

2. Is there any chance of a REPL, runnable at any Javascript engine?

Thanks, Rudy

raichoo hat gesagt…

Very little is unsupported by the new backend. Basically just the stuff that's related to C or lowlevel code, like Word8 and Word16 types. If you find anything that's not supported but think should be please file a bug and I'll take care of it if possible. I'm afraid I don't get the second question ^^, do you want REPL for Idris in the browser?

Anonym hat gesagt…

1. Okay, thank you.

2. Well, I knew the question is, well, how to put it friendly, ehm, nuts :-)

I just spend a bunch of time behind firewalls with no possibility to install haskell; or anything at all thats not a java library. So I started dreaming. Grin.

raichoo hat gesagt…

Nuts is good ^^.
Anyway, running a REPL in the browser would be a completely different ball game. Currently I'm just compiling Idris code to JavaScript and the compiler itself is not written in Idris. Don't dream, start hacking :D

Anonym hat gesagt…

Grin.