Lambda the Ultimate

The following article describes a verified version of the heapsort algorithm.

The verified heapsort algorithm is another example on how ghost functions/predicates can be used to describe loop invariants in a exact and concise manner.

It is easy to find questionable aspects of the javascript language, but there is at least one feature that it gets right: the composable concurrency model. The built in event loop and the continuation passing style allows completely different IO stacks, or many instances of the same stack to be easily composed in nodejs. Since every IO is asynchronous, the javascript programmer is forced to do the hard work and write code that fires as much asynchronous IO operation concurrently as possible, and to join the results in callbacks. This is not possible in a threaded programming language, since that encourages the programmer to write serial code, and the same holds if you use monads in Haskell which serializes all calls for you.

Here is an example application: suppose you want to traverse a large tree (directory structure or tree stored in a database) and print it out in a depth first fashion (or as an XML file with embedded child objects). If you use monads, then you will issue IO operations sequentially: first get the directory of the root, then the directory of the first child, then the directory of the first child of the first child, etc. However, the IO operations are slow, so you want to fire them concurrently. If you do this blindly, then you effectively do breadth first search as you issue IO operations, but then you have to store the results in memory to print it out in depth first, which will explode the memory overhead. Clearly, the best is some combination (use depth first search to drive the traversal, but at any point you issue extra queries that are expected to come soon).

Is it possible to write this depth first search concurrently in Haskell? The best would be to have a "handle" for file IO, or for socket IO, which you can use to serialize IO operations when necessary and execute IO parallel when necessary. I would like to execute operations A and B concurrently, but force the console IO to be serialized, however allow e.g. read only file IO to be parallel. I do not want to solve this problem by serializing the execution of A and B, only their console IO needs to be serialized. Is this possible?

So, LtU is 12!! I don't think this should go unnoticed. But as I was mostly quiet around here this year I am not qualified to offer a state of the lambda retrospective. Feel free to do so in the comments and, as they say, have some '(cake).

The Economist Language blog just posted an essay on the differences between computer code and natural language, taking a negative stance on their relationship. For all the talk of grammar, perhaps the title should have been "Why computer code isn't language".

Some of the qualities said to not exist in PL could be argued the other way ("dialects, idiolects, variation, natural change over time"). Additionally, though PL do not typically have some qualities mentioned, PL could and have been constructed to have some of these qualities mentioned in the article. Am I in the minority for thinking different than than article?