Ur/Web at Hac φ

I'll be giving a short talk and presentation on Ur/Web at the next Haskell Hackathon, Hac φ. The talks are scheduled to be between 10-15 minutes, so I'm aiming to have a short spiel for the people who are there in person. But I'm also keeping the slides fairly complete and detailed as possible for those who are interested, but won't be able to make it. I know, slides aren't the best, but I don't think there will be any video recording for the talks, so I'll try to make them as self-contained as I can.

On that note, Pandoc is awesome.

If you're going to be there or want to talk, get in touch with me!

Edit: It's been done, and Hac Phi was a ton of fun! I didn't get the slides as complete as I wanted to (partially due to laziness, gaming and a million other things,) but for the interested, you can find the slides online here.

OPA: now open source

I've been doing a bit of programming with Ur/Web and OPA in the last week, because they're both pretty similar frameworks in some sense, but with a lot of important differences. I'll maybe write something about this soon.

But in the mean time, OPA has now gone open source! No more need for an invite, so go grab it yourself: https://github.com/MLstate/opalang

opaque: blogging software written with Opa

A week or two ago, I was invited to the Opa private beta. Opa is basically a statically typed functional programming language designed for writing web applications. Yes - Opa is a programming language. And it's more than just that - Opa includes its own database server, as well as its own HTTP server. As a result, when you write programs, the result of the compiler is a single executable file that you can run and have 'just work.' Furthermore, when coding, both client-side and server-side code are written using the same language, and code that runs on the server is compiled to native code, while client side code is compiled to JavaScript. Another selling point of Opa is that you can automatically scale it across multiple machines and use a HTTP load balancer along with it (currently haproxy.) There is nothing special involved in doing this. You just have to run your executables using opa-cloud, and it'll "just work." This also applies to the database, and even real-time client-side updates that may be posted to all current visitors.

I also recently signed up for projectaweek, a small movement started by Mark to try and emulate the ferocious productivity of Don, and the goal is simple - to release 1 project a week, no matter if it is incomplete or partially busted, but it can't be late. So I put the two together, and decided to write something over the past week using Opa. The result is some simple blogging software that I've named opaque.

Right now it's pretty primitive. It displays posts though, and you can read it, and that's what counts! But it does have:

• Syntax highlighting (via SHJS)


• MathJax support (via MathJax CDN)


• Markdown support for entries (via upskirt)

Which I think are pretty necessary for anything that's to be taken even remotely seriously.

I was ridiculously happy with how easy it was to write, honestly. The trick is that you can write programs which are, in reality, asynchronous or stateless between client/server, in a nice, imperative/functional style, and the compiler just "does the rest" and transforms it appropriately. Also, because you write client and server side code in the same language, you get type checking on both client and server side, and so the compiler can eliminate certain classes of errors between the two. Opa's type system apparently is apparently a bit more powerful than say, ML or Haskell's, and lacks the existence of principal types (and thus may require some type annotations,) but overall the amount of type annotations needed is nearly zero. At least in my case. The compiler can also apparently catch other classes of errors, but I haven't looked into it, nor the type system (it'll have to wait for source code to be released.)

Opa isn't publicly available at the moment - it's an invite only preview. Source is coming. And it's very much worth noting that once the source is released, it will be AGPLv3, meaning any apps even written with Opa will need to be licensed under the AGPLv3 as well, unless you buy a license from MLState.

I have some invites still available for the Opa preview, before it goes open source, so you can try it before then. Feel free to contact me if you'd like one. I'll also probably be writing a little bit more about Opa up here with some examples, as well as a comparison between it and the formidable Ur/Web.

Now it's time to go play The Witcher, as I've clocked in my project this week.

RC4 in Haskell

I've been meaning to try out Levent Erkok's sbv library, but for a while I couldn't think of anything to write. Now I have, and it was quite fun to implement: RC4 in pure Haskell. I took the original RC4 code from cypherpunks, and rewrote it using sbv.

It took a lot of tweaking to get my implementation right, but I think it works correctly now.

Everything, including implementation, haddock documententation, a few tests and a few theorems all weighs in at ~275 lines. Most of it I somewhat directly translated from the cypherpunks posting. I also included a ByteString interface that matches the RC4 code in the cryptocipher package, and an instance of crypto-api's StreamCipher class. So you can actually use it for encrypting things. I make no means of guaranteeing any sort of efficient implementation; indeed, it's probably somewhat slow. If I can think of a good benchmark, I'll add some. But I enjoyed writing it, and sbv is a very nice DSL that was pretty easy to get used to.

The nice thing? This:

*RC4> proveRc4IsCorrect
** Elapsed problem construction time: 16.360s
** Elapsed translation time: 0.000s
** Elapsed Yices time: 34.084s
Q.E.D.
*RC4>

Which showed my proposition decrypt (encrypt x) == x was correct for 40 bit keys and 40 bit plaintexts. I was quite glad that yices could actually verify this. But despite the fact my proposition holds according to the SMT solver, I also did some testing of my implementation by QuickCheck testing it against cryptocipher's RC4 module. Sure enough - my QuickCheck tests quickly turned up problems!

Moral: don't trust code that's proven and has not been tested, as Wouter said (PDF.) Of course in this instance, proving encryption followed by decryption is the identity function isn't a huge breakthrough, nor is the fact my tests showed errors surprising. Due to RC4's symmetric, pseudo-random nature, the generation of the keystream can be wrong and this proposition will still hold. This was where the bugs lied: keystream generation. Nonetheless, just getting a proposition and blasting it with the solver to be told it's correct is quite satisfying and it did save me once or twice - I really like this SMT solver approach.

I haven't done the C code generation yet. It mainly has to do with the fact the interface would be horrendous because the generated C code cannot use arrays. Levent is working on a new version of sbv that will let you generate code using arrays though (we need this for the S state of the RC4 context, which is a 256 byte array.)

Anyway, here's the code. It also includes my version of the original C implementation from cypherpunks - mainly just a simple driver program with a test inside of it. Caveat emptor: I am not a cryptographer, issues may exist, etc.

I imagine with more compiler backends, it could be possible to have libraries of code written in Haskell using sbv that can then be verified, and extracted to other languages for use - it will also hopefully be extended to use other SMT solvers directly besides Yices. Maybe in future posts I'll write some tutorials for it or something.

QuickLZ compression for haskell

I've finished off a binding to QuickLZ for Haskell, available here. It has a very simple interface and allows you to compress strict bytestrings very easily. It uses QuickLZ v1.5.0, compression level 1, and has support for overlapping decompression too.

Currently there's no implementation for lazy bytestrings. I'm looking into enabling the streaming mode, so you can have a lazy interface, and also wiring up the result to John's enumerator package so you can write enumerator based compression code. I'm currently hitting a strange segfault however when defining a non-zero QLZ_STREAMING_BUFFER flag for the QuickLZ code, so I'll have to investigate that (and make sure it's not just me doing something dumb.)

Comments welcome.

First post

Don't panic.