Montag, 24. Juni 2013
Freitag, 31. Mai 2013
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:
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
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
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
Mittwoch, 13. Februar 2013
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:
However, it gets even worse. The above program can be written in a different way. Let's give it a try.
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:
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
Here's the result:
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!
--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!
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:
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
Operations on arrays are declared like this:
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.
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 indexWorking 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:
Now lets use the FFI to call into JavaScript land!
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:
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
Samstag, 4. Februar 2012
Setting up a Tor Bridge Relay on illumos
Times are getting rough again. There are regimes out there that censor the ability of their citizens to express themselves or communicate with each other, sometimes even lives are at stake. Communication isn't a luxury, it's what makes us human, it empowers us, tears down walls between people and helps us to understand each other. Censorship and total surveillance is a violation of human rights, it's something we need to fight.
One way of doing this is to support the Tor Project. In this blogpost I will show how to set up a so called bridge relay on illumos, an entry point to the tor network which empowers people that suffer under the influence of censorship and surveillance to access the internet.
Step 1: Building Tor under illumos
Building Tor is easy as pie. All you need is the libevent src and the Tor src.
Step 2: Setting up an illumos zone
Since illumos inherits all the awesome features of OpenSolaris we can isolate our Tor bridge inside of a zone. We will create a zone with the name "tor".
Before we start we need to create a zfs dataset for our zone. I usually put mine in /export/zones (which itself is a dataset) like so:
Step 3: Setup TOR
Time to get serious. After building Tor and putting it into our zone we now need to configure Tor to function as a Bridge Relay. Here we set up our bridge to listen on port 443. Since Tor traffic looks a lot like SSL it's a good place to run. Our
I recommend that you set up a tor user to avoid running as root. The problem is that you cannot run run a server on a privileged port when you are a mere user. We can use RBAC to give the tor user a profile that allows it to run services on such ports.
If you want to know more about the Tor Project, I recommend you this talk:
Step 1: Building Tor under illumos
Building Tor is easy as pie. All you need is the libevent src and the Tor src.
Step 2: Setting up an illumos zone
Since illumos inherits all the awesome features of OpenSolaris we can isolate our Tor bridge inside of a zone. We will create a zone with the name "tor".
Before we start we need to create a zfs dataset for our zone. I usually put mine in /export/zones (which itself is a dataset) like so:
[root@lain:~]> zfs create rpool/export/zones/tor[root@lain:~]> zonecfg -z tortor: No such zone configured
Use 'create' to begin configuring a new zone.
zonecfg:test> create
zonecfg:test> set zonepath=/export/zones/torzonecfg:test> verify
zonecfg:test> commit
zonecfg:test> exit
[root@lain:~]> zoneadm list -cv
ID NAME STATUS PATH BRAND IP
0 global running / native shared
- test configured /export/zones/tor ipkg shared [root@lain:~]> zoneadm -z tor install[root@lain:~]> zoneadm -z tor boot
[root@lain:~]> zlogin -C torStep 3: Setup TOR
Time to get serious. After building Tor and putting it into our zone we now need to configure Tor to function as a Bridge Relay. Here we set up our bridge to listen on port 443. Since Tor traffic looks a lot like SSL it's a good place to run. Our
torrc should look like this:SocksPort 0
ORPort 443
BridgeRelay 1
Exitpolicy reject *:*I recommend that you set up a tor user to avoid running as root. The problem is that you cannot run run a server on a privileged port when you are a mere user. We can use RBAC to give the tor user a profile that allows it to run services on such ports.
[root@tor:~]> usermod -K defaultpriv=basic,net_privaddr tor
[tor@tor:~]> pfexec tor -f torrcIf you want to know more about the Tor Project, I recommend you this talk:
Mittwoch, 4. Januar 2012
Building GHC under Illumos
I like the bleeding edge, that's why I always want to have the newest compilers for my favorite languages and Haskell is one of those languages. In this blogpost I'm going to show you how to build the latest and greatest GHC on the Illumos distribution OpenIndiana. If you don't want to build it yourself you can pick up a fairly recent version of GHC from the SFE Repository.
To make things easier let's get our hand on a GHC binary from which we can bootstrap our environment, luckily there is a package for GHC 7.0.3 for Solaris which works just fine under Illumos. Just install it and put it in your PATH environment variable.
Due to it's Solaris heritage, Illumos currently ships with a pretty outdated version of GCC. I recommend that you install the GCC provided by the SFE Repository since the shipped version causes some linking problems when dealing with the hidden attribute. If you have to use the old compiler you can get rid of this issue by using this quick and dirty patch which just gets rid of some pragmas and macros:
diff --git a/includes/Rts.h b/includes/Rts.h
index 91ec76d..adbbe54 100644
--- a/includes/Rts.h
+++ b/includes/Rts.h
@@ -52,7 +52,7 @@ extern "C" {
// with visibility "hidden" to hide them outside the RTS shared
// library.
#if defined(HAS_VISIBILITY_HIDDEN)
-#define RTS_PRIVATE GNUC3_ATTRIBUTE(visibility("hidden"))
+#define RTS_PRIVATE //GNUC3_ATTRIBUTE(visibility("hidden"))
#else
#define RTS_PRIVATE /* disabled: RTS_PRIVATE */
#endif
diff --git a/rts/BeginPrivate.h b/rts/BeginPrivate.h
index 6471b92..1af4c90 100644
--- a/rts/BeginPrivate.h
+++ b/rts/BeginPrivate.h
@@ -6,5 +6,5 @@
error: visibility attribute not supported in this configuration; ignored
*/
#if defined(HAS_VISIBILITY_HIDDEN) && !defined(freebsd_HOST_OS)
-#pragma GCC visibility push(hidden)
+//#pragma GCC visibility push(hidden)
#endif
diff --git a/rts/EndPrivate.h b/rts/EndPrivate.h
index 4cfb68f..c2e3154 100644
--- a/rts/EndPrivate.h
+++ b/rts/EndPrivate.h
@@ -1,3 +1,3 @@
#if defined(HAS_VISIBILITY_HIDDEN) && !defined(freebsd_HOST_OS)
-#pragma GCC visibility pop
+//#pragma GCC visibility pop
#endif
Now we are good to go. Get your hands on some fresh tarball, perhaps the latest and greatest RC. To configure your future GHC just run something like:
./configure --prefix=~/Library/GHC/version --with-gmp-includes=/usr/include/gmp
~/Library/program/version. From here I can manage everything using softlinks but feel free to use any other prefix.
Be sure to run the GNU Make (gmake) command and not the Illumos one. Sadly gmake seems to be unable to handle multiple jobs when compiling GHC so our final step looks like this:
gmake && gmake install
From here on you should be able to build pretty much every version you wish for. If you pick a version that is supported by cabal-install installing additional packages from hackage is a piece of cake. I usually have more than one GHC installed, the one that is shipped with the current Haskell Platform and the latest version with all the hot new features.
Illumos has the potential to be one of the best platforms for developing Haskell since it has exquisite DTrace support. If you want to help to improve the Haskell experience on Illumos, feel free to contact me in #openindiana on freenode.
Abonnieren
Posts (Atom)