Lambda the Ultimate

Two intensively studied intermediate representations in compiler theory are Static Single Assignment form (SSA) and CPS translations, and Richard Kelsey's 1995 paper, A Correspondence Between Continuation Passing Style and Static Single Assignment Form (.ps.gz) shows a nearly complete, exact equivalence between the two IRs.

The correspondence shows how the imperatively expressed SSA can be regarded as side-effect free, and Andrew Appel has pushed this idea to claim that SSA is functional programming. This result is of clear relevance to discussions turning on "what is purity?", such as here.

As an aside, the Wikipedia article Static Single Assignment form is rather good.

By now there is an extensive network of interlocking analogies between physics, topology, logic and computer science, which can be seen most easily by comparing the roles that symmetric monoidal closed categories play in each subject. However, symmetric monoidal categories are just the n = 1, k = 3 entry of a hypothesized “periodic table” of k-tuply monoidal n-categories. This raises the question of how these analogies extend. We present some thoughts on this question, focusing on how monoidal closed 2-categories might let us understand the lambda calculus more deeply.

Link to the talk

via The n-Category Café

Coding Horror is a popular programming blog. A recent post concerns type inference in C#:

C# ... offers implicitly typed local variables. ... It's not dynamic typing, per se; C# is still very much a statically typed language. It's more of a compiler trick, a baby step toward a world of Static Typing Where Possible, and Dynamic Typing When Needed.

... I use implicit variable typing whenever and wherever it makes my code more concise. Anything that removes redundancy from our code should be aggressively pursued -- up to and including switching languages.

You might even say implicit variable typing is a gateway drug to more dynamically typed languages. And that's a good thing.

I think this post is interesting for a number of reasons, and the link to LtU is just the start. Now it appears the author is confused as to what “implicitly typed local variables” are, confusing local type inference (which they are) with dynamic typing (which they are not). Many commenters also suffer from this confusion. Other commenters rightly note that the inferred type is not always the type the programmers wants (particularly important in the presence of sub-typing). Furthermore, type inference harms readability. I'm reminded of recent discussion on the PLT Scheme mailing list on the merits of local and global type inference. The consensus there seems to be that while local type inference is useful, global inference is not.

So, wise people, what is the future of type inference? How useful is it really, especially when we look at type systems that go beyond what H-M can handle? How are we going to get working programmers to use it, and understand it? Do we need better tool support? Do we have any hope of better education for the average programmer?

Bertrand Meyer yet again has lined up a fantastic set of speakers for this year's LASER summerschool that targets some very relevant and timely topics in our field:

• Tryggve Fossum, Intel Fellow and Director of Microarchitecture Development, Intel Corporation on Chip level Multi Processors
• Maurice Herlihy, Brown University on The Art of Multiprocessor Programming
• Bertrand Meyer, ETH Zurich and Eiffel Software on Correct Contract-Covered Concurrent Computation
• Robin Milner, Cambridge University on Bigraphs: a space for mobile interaction
• Peter O'Hearn, Queen Mary University of London on Proof Techniques for Concurrent Programs
• Daniel A. Reed, Microsoft Research and UNC Chapel Hill on Living in the Multicore Computing Clouds

Kilim is a message-passing framwork for Java that provides ultra-lightweight threads and facilities for fast, safe, zero-copy messaging between these threads.