Lambda the Ultimate

Since pi calculus is a hot topic lately, Pierce's Foundational Calculi for Programming Languages might be of interest as an introduction. It very briefly introduces and justifies foundational calculi in general, spends about 10 pages on lambda calculus, then builds on that with another 7 pages on pi calculus.

Some might want to check this /. thread,

On one particular problem instance (a garden of size 7x3), my C++ implementation finished in 1 second, while the OCaml implementation was still running after 16 minutes. Bear in mind that my OCaml implementation was dramatically faster than my equivalent Haskell code... If you write OCaml code that is isomorphic to C code, it will be fast---what about if you use OCaml the way it was meant to be used?

My critical view of this sort of thing is well known, and I don't want another holy war (the Knuth thread is enough for my taste), but I guess we should check comparisons of this sort from time to time, if only to keep everyone honest (including ourselves).

Nice surprise on my way to work this morning with an NPR story on Donald Knuth on the radio this morning. (Favorite quote: We are competing against ignorance).

Pitts and Gabbay, A New Approach to Abstract Syntax with Variable Binding, FAC 2001.

In the lambda calculus, the particular choice of variable names - even free variables - is irrelevant. Names serve two purposes:

• as mnemonics to help human readers understand their role, and
• to distinguish variables that are meant to be different and unify variables that are meant to be the same.

In a theory of binders, only the latter purpose is relevant. This is why it's so annoying to have to deal with capture-avoiding substitution, the Barendregt variable convention, gensym, and the like. These are all ways of getting around the fact that we've committed to a particular name when we really shouldn't have cared what the name was.

There are several standard ways to deal with this. Generating fresh names with gensym is awkward and forces the implementer to reimplement binding and substitution from scratch for each new object language; not to mention its violation of referential transparency. de Bruijn indices remove the variable names but are hard to read and understand. Higher-order abstract syntax implements binders in the object language as functions in the metalanguage, in order to reuse the built-in mechanisms of binding and substitution; but by mixing higher-order values in algebraic datatypes, structural induction is hard to recover.

This paper introduces a theory of fresh names that restores algebraic reasoning, referential transparency, and structural induction to algebraic datatypes with a HOAS-like notation for introducing binders into an abstract syntax. This is the set-theoretical basis for the authors' work on FreshML and FreshO'Caml, which we've discussed a little bit on LtU in the past.

(via Lemonodor)

Guy Steele leads a small team of researchers in Burlington, Massachusetts, who are taking on an enormous challenge -- create a programming language better than Java... Think of it as Java for scientists, Java for the programmers of a peta-scale supercomputer.

You just have to love this quote from Steele: I'm now not convinced that a single programming language can serve everyone's needs, because the needs are so diverse. Well, duh...

But obviously Steele knew this long ago. Anyway, Fortress seems to be concerned with notation ("with square root signs and exponents placed above the line"), in the hope that that's going to be enough to lure Fortran programmers. Time will tell.

Many recent threads in the discussion group refer to papers we discussed in the past. Some of these were discussed at great length.

I urge you to search the site when you want to refer to a paper that might have been discussed before, and to link to the original discussion of the paper, if there was one.

I urge the editors to post to the home page about important papers that first come up in the discussions currently going on.

Thanks!

(via Keith)

This interview describes some hacks that may interest you guys. Among them a ultra-simple threading library for C and interesting stuff concerning sensor networks.

via Wadler, via Josef Svenningsson

Language design luminaries Xavier Leroy, Simon Peyton Jones, Benjamin Pierce, and Philip Wadler plan a mini-conference to discuss a possible new language effort.

Attend their April 6, 2005 LINKS meeting at ETAPS in Edinburgh to participate. Schedule details say, "There is no requirement to register for ETAPS to attend Links."

I hope the confab attracts some Alice ML people.

Shriram Krishnamurthi's classic macro automaton example, well known from his LL1 presentation, is now written up as an educational pearl for JFP.

As you may recall, the example shows how to use Scheme macros to create an an automata DSL, and concentrates on the importance of proper tail-calls for achieving the desired semantics.

Linear forwarders are actually the basic mechanism of an earlier implementation of the pi calculus called the fusion machine. We modify the fusion machine, replacing fusions by forwarders. The result is more robust in the presence of failures, and more fundamental.

And also:

The point of this paper is to solve the problem of input capability with a language that is “just right” – it neither disallows more features than necessary (as does the join calculus), nor adds more implementation work than is necessary (as does the fusion machine).

Yes, these are the same capabilities as in capability-based security. I am looking forward to read the complete paper, as it seems to confirm my unclear ideas of how capabilities and various pi calculi are related.