Lambda the Ultimate

Nothing terribly exciting or newsworthy, but I suspect that many readers will find something to love in this blog post from Gilad Bracha. He starts by asking, "Why is static state so bad, you ask?" and goes from there...

Given all these downsides, surely there must be some significant upside, something to trade off against the host of evils mentioned above? Well, not really. It’s just a mistake, hallowed by long tradition... Static state will disappear from modern programming languages, and should be eliminated from modern programming practice.

From the introduction:

Seen in outline, the history of LC and CL splits into three main periods: first, several years of intensive and very fruitful study in the 1920s and ’30s; next, a middle period of nearly 30 years of relative quiet; then in the late 1960s an upsurge of activity stimulated by developments in higher-order function theory, by connections with programming languages, and by new technical discoveries. The fruits of the first period included the first-ever proof that predicate logic is undecidable. The results of the second attracted very little non-specialist interest, but included completeness, cut-elimination and standardization theorems (for example) that found many uses later. The achievements of the third, from the 1960s onward, included constructions and analyses of models, development of polymorphic type systems, deep analyses of the reduction process, and many others probably well known to the reader. The high level of activity of this period continues today.

Beware: This is a long paper (but less than you might expect it to be by looking at the page count: about half the pages are dedicated to the bibliography).

In the announcement on the TYPES Forum the authors invited comments, suggestions and additional information on the topics of the paper, namely the development of lambda-calculi and combinatory logic from the prehistory (Frege, Peano and Russell) to the end of 20th century.

When Is A Functional Program Not A Functional Program?, John Longley. ICFP 1999.

In an impure functional language, there are programs whose behavior is completely functional (in that they behave extensionally on inputs) but the functions they compute cannot be written in the purely functional fragment of the language. That is, the class of programs with functional behavior is more expressive than the usual class of pure functional programs. In this paper we introduce this extended class of "functional" programs by means of examples in Standard ML, and explore what they might have to offer to programmers and language implementors.

After reviewing some theoretical background, we present some examples of functions of the above kind, and discuss how they may be implemented. We then consider two possible programming applications for these functions: the implementation of a search algorithm, and an algorithm for exact real-number integration. We discuss the advantages and limitations of this style of programming relative to other approaches. We also consider the increased scope for compiler optimizations that these functions would offer.

I like this paper because it shows how some of the most abstract bits of formal logic (realizability models of higher order logic) suggest actual programs you can write.

As a barely-related aside, even a brief look into this realizability stuff also taught me a good deal of humility -- for example, it seems that at higher types, what you can represent mathematically depends on the specific notion of computation you're using. So the mathematical consequences of the Church-Turing thesis are rather more subtle than we might initially expect. (Andrej Bauer discusses a related point in more detail in this blog post.)