Lambda the Ultimate

Philip Wadler has a pair of Links demos up and running. One is a to-do list (source) that runs on the server but keeps state on the client via continuations; the other is an input validator (source) that is translated into Javascript to run on the client. A sample of the latter:

<input l:name="word1" type="text" value="{word}"/>
{[ if word == "" then <font/>
   else if isdigit(word) then <font color="blue">ok</font>
   else <font color="red">error: {[word]} is not a digit as a word!</font> ]}

(Previous Links discussion on LtU)

Dynamic optimization refers to the runtime optimization of a native program binary. This paper describes the design and implementation of Dynamo, a prototype dynamic optimizer that is capable of optimizing a native program binary at runtime... Contrary to intuition, we demonstrate that it is possible to use a piece of software to improve the performance of a native, statically optimized program binary, while it is executing. Dynamo not only speeds up real application programs, its performance improvement is often quite significant. For example, the performance of many +O2 optimized SPECint95 binaries running under Dynamo is comparable to the performance of their +O4 optimized version running without Dynamo.

I think Dynamo is pretty well known, but in the light of the Apple switch to x86, it offers perspective on the possibility of using JIT compilation to translate binaries.

The application to programming languages is also straightforward.

It seems worthwhile to connect a few discussions we had recently, and perhaps put them in prespective.

Web programming is becoming more and more important, and many feel there's room for better programming language support for the style of programming is entails. One approach is, of course, to design dedicated (i.e., domain specific) programing languages, such as Links. The other approach is to build application frameworks, but this isn't as easy as it might sound, and depends on the underlying language features, for example continuations (continuations and web programming were discussed here many times).

Ajax style web applications may require multi-language programming, and pose their own set of software engineering difficulties. The Ruby on Rails framework (tutorial) supposedly handles Ajax very nicely, and is causing some developers to move in the direction of Ruby. Libraries and framework often have this effect, and influence language popularity more than fundamental language features. This is quite reasonable since, as we see repeatedly, it is quite difficult to appreciate a language by evaluating language features in isolation.

It might be helpful to consider what Ian had to say regarding Ruby on Rails as opposed to Python web frameworks.

I don't think the important issue at the moment is to decide which language is best. I think it is more important to identify the trends and establish if language design can help improve the state of the art, and if so where.

Personally, I think the answer is yes, and I mentioned some areas of opportunity before, but I'd be interested in hearing what others think.

While classically lambda-expressions are seen as trees, people don't stop trying to use more general graphs for their representation (according to the authors, the ideas go back to Bourbaki in 1954).
Bottom-Up beta-Substitution: Uplinks and lambda-DAGs

If we represent a lambda-calculus term as a DAG rather than a tree, we can efficiently represent
the sharing that arises from beta-reduction, thus avoiding combinatorial explosion
in space. By adding uplinks from a child to its parents, we can efficiently implement
beta-reduction in a bottom-up manner, thus avoiding combinatorial explosion in
time required to search the term in a top-down fashion. We present an algorithm for
performing beta-reduction on lambda-terms represented as uplinked DAGs; describe its proof
of correctness; discuss its relation to alternate techniques such as Lamping graphs,
explicit-substitution calculi and director strings; and present some timings of an implementation.
Besides being both fast and parsimonious of space, the algorithm is particularly
suited to applications such as compilers, theorem provers, and type-manipulation
systems that may need to examine terms in-between reductions—i.e., the “readback”
problem for our representation is trivial. Like Lamping graphs, and unlike director
strings or the suspension lambda calculus, the algorithm functions by side-effecting the term
containing the redex; the representation is not a “persistent” one. The algorithm additionally
has the charm of being quite simple; a complete implementation of the data
structure and algorithm is 180 lines of SML.

So it's efficient in both time and space, interactive, and simple to implement! What else is left to desire?

As Slashdot observes, PHP was born 10 years ago on June 8th 1995.

It's had its knockers, but it's running this site...

Could it be that our gracious host has gone and got himself appointed to the Scheme Language Editors Committee?

(via Michael Rys)

This is a Last Call Working Draft. Comments on this document are due no later than 15 July 2005...

I guess that those interested in this area know about this, and for others it is a bit too late to get involved, but at least it's good to know the status of the formal specification.

Although already mentioned before, I believe this paper (which reconciles two approaches to defining continuations) deserves a separate story.

On Evaluation Contexts, Continuations, and the Rest of Computation

Continuations are variously understood as representations of the current evaluation context and as representations of the rest of the computation, but these understandings contradict each other: plugging an expression in a context yields a new expression whereas sending an intermediate result to a continuation yields the final answer. We show that continuations-as-evaluation-contexts are the defunctionalized representation of the continuation of a single-step reduction function and that continuations-as-the-rest-of-thecomputation are the continuation of an evaluation function. Furthermore, we show that defunctionalizing the continuation of an evaluator gives rise to the same evaluation contexts as in the single-step reducer. The only difference is how these evaluation contexts are interpreted: a ‘plug’ interpretation yields one-step reduction, whereas a ‘refocus’ interpretation yields evaluation.

By now, shift/reset should be as popular as call/cc was ten years ago. Some think these control operators are even more important in practice than call/cc, and should be directly supported by PLs. I believe, this paper by Chung-chieh Shan will be interesting to many who loves logic and Curry-Howard isomorphism.

From shift and reset to polarized linear logic

Abstract:

Griffin pointed out that, just as the pure lambda-calculus corresponds to intuitionistic logic, a lambda-calculus with first-class continuations corresponds to classical logic. We study how first-class delimited continuations, in the form of Danvy and Filinski’s shift and reset operators, can also be logically interpreted. First, we refine Danvy and Filinski’s type system for shift and reset to distinguish between pure and impure functions. This refinement not only paves the way for answer type polymorphism, which makes more terms typable, but also helps us invert the continuation-passing-style (CPS) transform: any pure lambda-term with an appropriate type is beta-eta-equivalent to the CPS transform of some shift-reset expression. We conclude that the lambda-calculus with shift and reset and the pure lambda-calculus have the same logical interpretation, namely good old intuitionistic logic. Second, we mix delimited continuations with undelimited ones. Informed by the preceding conclusion, we translate the lambda-calculus with shift and reset into a polarized variant of linear logic that integrates classical and intuitionistic reasoning. Extending previous work on the lambda-µ-calculus, this unifying intermediate language expresses computations with and without control effects, on delimited and undelimited continuations, in call-by-value and call-byname settings.

Bidirectional fold and scan, O'Donnell ,J.T. In Functional Programming, Glasgow 1993, Springer Workshops in Computing.

Bidirectional fold generalises foldl and foldr to allow simultaneous communication in both directions across a list. Bidirectional scan calculates the list of partial results of a bidirectional fold, just as scanl and scanr calculate the partial results of a foldl or foldr. Mapping scans combine a map with a scan, and often simplify programs using scans. This family of functions is significant because it expresses important patterns of computation that arise repeatedly in circuit design and data parallel programming.

The biderctional fold is a bit surprising at first, but the real reason I am posting this is to encourage discussion on the connection between functional and data prallel programming.