Prophecies: future-generators

I've discovered a neat idiom. I have a web servlet that spawns a separate process and reads a bunch of terms from the process's output. I want to be able to view those terms one at a time in the web page, but I don't want to leave the process hanging indefinitely based on the user's interaction. At the same time, I want it to be safe for clone/back as all web programs should. So the program should be able to process the terms in a lazy fashion, and allow backtracking (without having to re-read terms after backtracking), but the actual reading of the terms should happen concurrently in order to close the separate process as soon as possible.

This is a sort of combination of generators, which allow programmers to separate producers from consumers, and futures, which are a concurrent variation of laziness, where evaluation of a subexpression can happen concurrently, but evaluation of the containing expression must block if it needs the value of the subexpression.

Let's call these future-generators "prophecies." We create a prophecy with a special syntax whose subexpressions are evaluated immediately but in a separate thread from the creator of the prophecy:

(let ([p (prophecy
         (yield 1)
         (yield 2)
         (yield 3))])
...)

The difference between this and traditional generators is that yield does not halt evaluation in the current local evaluation context, which is happening in a separate thread. It simply queues up the value to make it accessible to the rest of the world.

We can access the yielded values with a library function prophecy-next, which takes a prophecy and blocks until there is a value available, or raises the sentinal value stop-iteration to indicate that "the prophecy is fulfilled."

Or we can extract the values lazily with a stream with prophecy->stream, which produces a stream, where (streamof a) = (promiseof (union null (cons a (streamof a)))).

Now my servlet is easy to write:

(define (start request)
(let ([p (prophecy
           ... (launch "prog.exe") ...
           (let loop ()
             ... (yield (read-term)) ...)])
 (go (prophecy->stream p))))
(define (go stream)
(if (null? (force stream))
    `(html (body "DONE"))
    (send/suspend/dispatch
      (lambda (proc->url)
        `(html
          (body
           (p ,(format "~a" (car (force stream))))
           (p (a ([href ,(proc->url (lambda (req)
                                      (go (cdr (force stream))))
                 "Next"))))))))

The separate program launches immediately, and all its output is read in as soon as possible. But the terms are packaged up via a prophecy into a lazy stream, which the web servlet reads in one page at a time. Users can safely backtrack, clone windows, and/or refresh any of the pages in the interaction, and the values always appear in the proper sequence, without ever having to regenerate them from the separate process.

---

Update: Added to PLaneT.

Formalizing JavaScript

Last week I gave a talk at the UCSC Software Engineering Seminar entitled Formalizing JavaScript.* I talked about the approach I've been taking to specifying the operational semantics of JavaScript, in terms of both the formal approach to the model and the engineering of the executable model.

---

*You'll probably want a better cursive font than Comic Sans MS, such as Monotype Corsiva, Textile, or one of the Chancery fonts.

---

Update: I've written up some notes to accompany the talk as well.

Customized literals in ECMAScript 4

One neat little feature that has come up in the design of ECMAScript Edition 4 is the ability to define conversions between datatypes. Class-based OO is nice for some purposes, and is certainly popular, but the ability to use syntactic literals to construct data is nice, and usually disappears when you "upgrade" to a bondage-and-discipline language like Java.

In ES4, it looks like you'll be able to define a sort of customized literal syntax for any class by means of an automatic conversion method. For example, imagine the following code:

var kleinBlue : Color = [ 0x00, 0x2F, 0xA7 ]
...
kleinBlue.toCMYK()
...

We can define a Color class with whatever methods we want (such as toCMYK) while still constructing one with a simple, lightweight array literal syntax.

We achieve this by defining a conversion method on the Color class:

class Color {
    ...
    type RGB = [ UInt, UInt, UInt ]
    function to(triple : RGB) {
        type switch (triple) {
            case ([ r, g, b ] : RGB) {
                return new Color(...)
            }
        }
    }
}

Now any context expecting the type Color can also accept an RGB triple and automatically convert it to an instance of Color.

ECMAScript reference values

Try this in SpiderMonkey or Firefox:

function foo(flag) {
    if (flag) {
        print('hello') = 10
    }
    return 42
}

foo(false) // 42
foo(true)  // SyntaxError: invalid assignment left-hand side

Solving today's web problems

Gilad Bracha's provocative Will Continuations Continue? has stirred up some controversy this week. His objection to continuations stems from the observation that in Ajax applications, the back button is less important than in traditional web programs, sometimes even effectively disabled. For an architect deciding whether to implement continuations for a web framework or its underlying VM, this has to alter the equation. Are Ajax applications rendering continuations obsolete? [1]

I'm a little late to respond, thanks to several days of netlessness. Gilad's post has generated some thoughtful discussion: Tim Bray protests that the web's simple UI model is well understood by users, Don Box points out that the web is not necessarily the only killer app for continuations, and Avi Bryant explains a few of the different kinds of state in web applications and where continuations fit into the picture. Later, Ian Griffiths raises deeper technical complaints about server-side continuations persistence about resource management (what happens when the user walks away?) and thread migration; Ezra Cooper responds that these problems don't exist for Links, where continuations live on the client side.

What makes Gilad's argument unrealistic is that Ajax applications currently account for some miniscule percentage of the web. Even if interactive applications are the future, the web never forgets its past. It's as naive to think you can stop supporting the back button as it would be for browsers to stop supporting HTML 4. You could protest that only the browsers have to support these "legacy" web pages, whereas on the server side, web programmers should start writing Ajax apps right now. But I don't see amazon.com or hotwire.com throwing away their shopping carts in favor of a Ruby on Rails codebase. There are way more existing applications with huge codebases that could benefit from a backwards-compatible solution to the Orbitz problem than there are companies itching to throw their entire codebase away to make way for an all-Ajax site.

None of this changes the fact that adding continuations to the JVM isn't easy. It's still a design decision with the attendant trade-offs. But speculation that everyone will be writing programs that make no use of the back button, say, 10 years from now, is not a compelling excuse not to support those programs now.

---

[1] As a pedantic aside, continuations could no more become obsolete than variables, or functions, or algorithms could. Continuations are an abstract concept, not a programming construct. More precisely, the real question is whether Ajax applications are rendering obsolete the use of first-class continuations as an implementation strategy for web application frameworks. In particular, I think a number of people have the misconception that programmers have to understand and use call/cc in order to program with these frameworks. In fact, the frameworks only use continuations under the hood to allow the programmer to write their web programs in a natural style.

Late and early binding

It's taken me a long time to figure out what people mean when they talk about "late binding" and "early binding." Little by little, I was beginning to get a handle on it, when Brendan showed me this Python spec which used the terms to refer to order of expression evaluation in a syntactic form! According to the spec's terminology, evaluating an expression earlier is ostensibly "early binding." This freaked me out, but Brendan reassured me that this was probably just a misuse of terminology on the part of the Pythonistas.

At any rate, as I understand them, late and early binding describe the point in the lifetime of a computer program (usually, compile-time versus runtime) at which a particular variable reference becomes dereferenced, i.e., at what point its binding is discovered. Lisp, which is dynamically scoped, doesn't dereference function arguments until runtime, based on the dynamic context. Scheme variables, by contrast, can be early bound, since all variables' bindings are based on their lexical scope. Dynamic dispatch is another instance of late binding, where method names are resolved at runtime.

Dynamic scope is generally regarded as a liability, because it completely violates abstractions, exposing programmers' choice of variable names and making them vulnerable to accidental capture. Dynamic dispatch is a somewhat more restricted form of late binding, where the programmer has finer control over what names can be overridden by unknown external parties.

Compiler writers like early binding because it's an opportunity for optimization--variable references can be compiled into direct pointer dereferences rather than map lookups. From the perspective of program design, early binding is good because it results in clearer programs that are easier to reason about. However, in certain restricted forms, late-bound variables can be useful as a way of leaving a program open to subsequent extension. This is the purpose behind dynamic dispatch, as well as implicit parameters such as in MzScheme or Haskell.

Resumable exceptions

One more thing I learned from Avi: there's a simpler way to implement resumable exceptions than the way I'd thought of. Having been perverted by my formative years as a Java programmer, I always assume the meaning of throw was carved in stone tablets:

1. Thou shalt abandon thy current context.
2. Thou shalt unwind the stack, verily, until thou findest the first handler.

So my solution involves capturing the continuation at the point of the throw, to allow the handler to reinvoke the continuation, effectively resuming at the point where the exception occurred. But why waste time unwinding the stack, if you're only going to put it right back in place? The Smalltalk solution (and I believe the Common Lisp solution as well) is to leave it up to the handler to decide whether to unwind the stack. In other words, throw (I think it's called raise in Smalltalk) simply causes the runtime to crawl up the stack, which it leaves intact, to find the first handler, and lets the handler decide whether to unwind, i.e., to blow away the portion of the stack between the throw point and the catch point.

I suppose this means the handler runs on top of the portion of the stack where the raise happened, and there must be some provision for what to do if the handler finishes without a control operation; presumably this would have the same behavior as resume nil, or however you'd express "don't unwind the stack; resume where the exception occurred; but I don't have any useful result value for the failed operation."

My introduction to Smalltalk

Another highlight of my trip to Amsterdam this week was meeting Avi Bryant, of Seaside fame. We talked about Smalltalk, web programming, and his latest project, Dabble. In the past, I've had trouble knowing where to begin with Smalltalk, so he sat down with me and walked me through building a simple program. It was enough to give me a flavor of the language, and to get me started if I want to experiment with it at some point (no time these days!). It's an absolutely breathtaking language. I am still skeptical about excessive reflection. It's clearly extremely powerful, and attractive in its conceptual simplicity. But I generally favor a careful balance between expressive power and local reasoning, and Smalltalk seems to tip awfully far towards the former. Nevertheless, I'd need to learn more and build real systems in Smalltalk before making judgments.

The way Avi designed Seaside leads to a beautiful style of web programming. Of course, there's the fact that the control flow is both compatible with the back button and window cloning and written in a natural style, thanks to continuations under the hood--but that's no surprise. It's in fact roughly the same approach as send/suspend/dispatch (though with the rather more friendly method name renderContentOn). But what I really enjoyed was the object-oriented approach to modeling the components of a web page.

In Squeak, essentially every component in the entire VM--numbers, blocks (closures), windows, stack frames, metaclasses, you name it--is represented as a Smalltalk object, with some particular set of supported methods and various ways to view it. The "system browser" provides a useful view: it introspects the object for its properties and their values, its methods and their source code, and any associated documentation, and displays them in an informative GUI window.

In Seaside, web pages can be seen as simply a different view on objects (that have special methods for rendering on the web, of course). When you change properties of a web component, its web view changes accordingly. Usually, these changes in state are triggered by user actions via the web: clicking links or submitting forms. If you change the property through the Squeak UI, then you can just reload the web page to see the changes. Most impressively, if you change the source code of a method on the object--say, the code that responds to a user action--there's no need to reload whatsoever! The next action simply invokes the method, which now happens to have a new implementation.

Exciting week!

I've had an exciting week in Amsterdam, attending XTech 2006 thanks to the generosity of Mozilla. On Thursday I visited Eelco Visser and Martin Bravenboer at the University of Utrecht. It was a fun and productive visit.

In the last couple of months I have started using Stratego/XT to model the semantics of ECMAScript. I believe that it's possible to scale the semantic frameworks that we use in research up to model whole, industry-sized programming languages. Now, these modeling frameworks are formal systems, just like programming languages themselves. So it should also be possible to express these models in a machine-executable form. There are several benefits to this approach:

1. The added rigor that comes from the level of detail and precision required to get a machine to understand the model.
2. The ability to test actual ECMAScript programs against the model.
3. A reference implementation against which implementations can be tested.
4. The eventual possibility of applying automated reasoning tools to the model (though not immediately!).

A particularly attractive feature of Stratego is its extremely customizable syntax. I have been able to use this to be very particular in defining the "syntax of the semantics" to maximize its readability.

Eelco and Martin liked my model--they found the CEKS machine representation of continuations lovely--and are glad to have an interesting application of Stratego. We talked about some of the things I could do better (and they already found a few subtle bugs in my implementation) as well as a couple of requests I had for Stratego. They're interested in what kinds of optimizations they could apply to their compiler that would provide the most benefit to applications like mine. For instance, since my abstract machine generally operates on only a few small forms that have fixed shapes, deforestation might be applicable.

Martin is now working on implementing the ECMAScript grammar, which is notoriously difficult to express in traditional parser generation frameworks. The module grammar formalism SDF, based on Tomita's generalized LR parsing algorithm and used in the Stratego/XT system, should actually allow us to define the syntax quite elegantly. This will allow us to parse actual ECMAScript programs, as well as to model eval realistically, since it relies on parsing strings as ECMAScript programs.

Syntactic capital

When you step outside your familiar community, you learn interesting things about your assumptions. Something I've learned on the ECMA committee is that in Scheme, new syntax is "cheap," but not so in other languages.

Because syntax definition is in the hands of Scheme user programmers, we expect to see new syntactic forms all the time. As a result, implementing a feature as a syntactic form is uncontroversial in Scheme. In other languages, however, a new syntactic form signals (at least intuitively) a global change to the language. Users know that a new API is something they can put off learning until they feel they need it. But if there's a syntactic form in a language that you don't understand, you feel as though you don't have a handle on the language.

In terms of pragmatics, it's easier for language implementors to implement a subset of an API than it is to implement a subset of the syntax; you can at least guarantee that all programs will parse the same. What this really comes down to is scoped syntactic extensions, i.e., macros. If you can modularize syntactic forms, you can signal a parse error that says "I'm sorry, I don't support this syntactic form," which is the same as "I don't support this API."

In terms of cognitive load, modularizing syntactic forms allows users to learn subsets of a language in exactly the same way they learn subsets of libraries.

Lightweight

One possible definition: avoiding unnecessary abstraction.

Jewels of the lambda calculus: scope

If abstraction is the grand prize-winning jewel of the lambda calculus, then scope is the first runner-up. Mitch Wand teaches his graduate students that the scoping properties of a language are one of the Four Questions we ask in order to understand its semantics ("why is this language different from all other languages?").

Scope is the first static property of any programming language. Lexical scope gives us a static context in which to understand a fragment of a program. Within the following program:

λy.λx.y

we can look at the inner portion, λx.y, and in order to understand what portion of the program gives meaning to its body, we must understand that y is bound to--i.e., will receive its runtime meaning from--the static context of the fragment that binds it, i.e., the outer binding.

The static aspects of a program are what communicate its properties to the reader, allowing the reader to understand its behavior logically, as opposed to experimentally. Scope is the property that communicates the relationships between fragments of a program, whether through arguments, module imports, or class hierarchies. Scope is the static assignment of responsibility to these units of the program for communicating dynamic information.

Jewels of the lambda calculus: abstraction as generalization

Since there are few things as likely to inspire in me a sense of religious reverence as the lambda calculus, I've decided to start a new series on some of the deep principles of computer science lurking in the lambda calculus.

Let's start with the crown jewel, abstraction:

λx.e

This simple form represents the first rule of programming. Ruby hackers call it the "don't repeat yourself" rule. Perl hackers call it laziness: good programmers avoid repetitive, manual tasks. No matter the size, shape, or form, any time you write a program, you create an abstraction, a piece of code that automates a common task that otherwise would have to be repeated by a human.

Lambda abstractions represent the generalization of repeated patterns by parameterizing over their differences. If you perform several computations that are similar but not identical:

(9/5 × 23 + 32)
(9/5 × 40 + 32)
(9/5 × 13 + 32)

then each one of these computations is a special case of a more generalized procedure. The abstraction of the three is represented by parameterizing over the portion where they differ:

λc.(9/5 × c + 32)

From functions to abstract classes to Microsoft Office macros to parametric polymorphism, every form of abstraction is at its heart this same phenomenon.

Stratego is cool

I've been meaning to talk about this for a while. Stratego is a very cool language. Their raison d'être seems to be performing program transformations, such as compilers and program optimizations. But because it's a term rewriting system, it's also perfectly reasonable to use it as a framework for specifying operational semantics of programming languages.

Here's an example rewrite rule, specifying the evaluation of variable references in a CEKS machine:

EvalVar :
  |[
     Expr:  $e,
     Env:   $r,
     Cont:  $k,
     Store: $s
  ]|
→
  |[
     Value: $v,
     Cont:  $k,
     Store: $s
  ]|
where <is-var> e
    ; x := <var-name> e
    ; v := <resolve>(x,r)

Unless you know Stratego, you won't realize the most remarkable thing about this code: it's using a custom syntax for the representation of the configurations in the CEKS machine! That is, I've extended the syntax of Stratego with a concrete syntax for configurations, bracketed between |[ and ]| tokens. I've also added unquotation to that concrete syntax in the form of $ tokens followed by Stratego terms. This allows me to bind meta-variables within the left-hand side of the rewrite rule and the where clauses and refer to bound meta-variables within the right-hand side of the rewrite rule and again in the where clauses.

Stratego is based in part on SDF, the Syntax Definition Formalism, which is a lovely system for defining modular grammars. SDF is based on Tomita's Generalized LR (GLR) parsing algorithm, which recognizes the full class of context-free grammars, even ambiguous ones. If you want extensible grammars, you have to work with a class of grammars that's closed under composition, so they've chosen the most permissive, the full CFG class. Unfortunately this means you can end up with ambiguities, but as far as I know I haven't run into any sneaky ambiguities yet.

The other important feature of Stratego is its computational meta-language. My two requirements for a term rewriting system were the ability to specify rewrite rules in terms of the concrete language, which Stratego provides with flying colors, and the ability to compute side conditions. Stratego's entire computational model is based on rewriting, so side conditions work by saving the current state of the world and performing a rewrite on the side. Their rewriting combinators, known as strategies, allow for some pretty powerful abstractions. It has the feel of programming in the backtracking monad, not unlike Prolog. It's a little unfamiliar for a functional programmer, but it's perfectly adequate for the job.

It is my hope, and I'm optimistic, that we'll use Stratego to model the whole of the ECMAScript Edition 4 semantics. It's not on the same level as modeling the language in a theorem prover and using it to prove safety properties of the language mechanically, but my experience so far has shown that just having an executable model of a language is extremely useful for testing and driving out bugs in the semantics.

Java module system

Fascinating! There's a Java module system in the works.

Huzzah!

I finally have a working DSL connection at home! Now I can submit those few cherished hours of daily rest to the will of the Great Lord Productivity.

On a related note: in the year 2006, setting up DSL shouldn't take a week of phone tag, a dozen tech support reps, and an entire day wasted on troubleshooting (after the technician finishes repairing the line). I think my favorite moment was when the precious phone rep announced "I've figured out what the problem is! You're not actually using Internet Explorer, you're using a web browser with a bug that it doesn't display web pages." Thanks, Sherlock.

How do you say "maybe"?

• Haskell, ML: Maybe T, T option
  
• Scheme: either T or #f
• Java, C#: either an ordinary T or null
• ML, Scheme, Java, C#: either a value or an exception
• Prolog: success or failure

C rots the brain

It's high time for a good rant. I'll warm up by quoting Cassandra:

I'm sorry to be politically incorrect, but for the ACM to then laud "C" and
its inventors as a major advance in computer science has to rank right up
there with Chamberlain's appeasement of Hitler.

One of our nastiest inheritances from C is a set of ingrained assumptions about the implementation of the control of any programming language.

Consider the pure lambda calculus. Application of a β-redex completely replaces the application node with the body of the function being applied. That is, there is never any space consumed in the representation of control for a procedure application. Rather, it is when one of these applications occurs in the context of some other computation that the program's control consumes space. To quote Guy Steele:

Intuitively, function calls do not "push control stack"; instead, it is argument evaluation which pushes control stack.

A continuation frame represents a kind of to-do list of what the program has left to do. It only needs to save this information in memory somewhere if it's going to do something else first, i.e., call another procedure.

The pernicious legacy of C is that we assume entry to a procedure body must always create a stack frame. But what is this frame for? It keeps a finger on our current point in the program, i.e., the program counter, and perhaps it stores some local data that we'll need in order to complete the evaluation of the function. If the procedure happens to be a leaf procedure, i.e., does not make any function calls, there's no need to save the current position, since we're not going anywhere else. Or maybe the procedure only conditionally calls another procedure. In that case, we might not need a continuation frame until we jump to the particular branch that is guaranteed to make the procedure call.

The assumption that procedure calls must push stack is so built-in to my head that I constantly have to remind myself: procedure entry and continuation frame allocation are not necessarily correlated!

But now the true folly is in the representation of the continuation as a simple stack. Gone are the days where we were told "if you want a string, just allocate a fixed buffer that's really, really big and hope you never need any more than that." (Well, gone should be the days.) Why then do we only get a fixed buffer size for the single most important part of every single program, the program's control itself? It's absurd to have your program tell you, "other than, like, those couple of gigabytes sitting over there, I'm totally out of space."

Why do these silly limitations persist? Because C rots the brain.

Update: Sam doesn't think it's fair for me to blame C. I guess C has been the drug that led to my personal brain damage, but it's perfectly possible for programmers of older generations to have been addled by Algol or Fortran, or newer generations by Java or C#. There's plenty of blame to go around...

Why the CPS simulation of CBV works

Incidentally, it's exactly the common element of call-by-name and call-by-value I mentioned a moment ago that facilitates the CPS simulation of call-by-value in call-by-name. Both reduction rules require that the operator of a redex be a value. In either calculus, reduction relies on instantiating a bound variable within the body of a function; there's no obvious way you could know how to reduce if you don't actually know what the operator is. So both systems force evaluation of an operator in order to evaluate an application. The difference is whether you also force the operand.

The CPS transform just makes it so that all evaluation within an entire program occurs exclusively in operator positions. After the translation, all operands are values and therefore irreducible. This property is also preserved under reduction, so at every step, a CPS'ed program behaves the same in either calculus.

In other words, if every operand is always a value, there's no difference between the β-rule and the β_v rule.

Observable differences between reduction strategies

It's easy to misunderstand the difference between lazy and eager evaluation. You might be tempted to think that 1) lazy evaluation does reductions from the "outside in," meaning that finds the outermost redex and reduces it before reducing its subterms, and 2) eager evaluation, by contrast, reduces from the "inside out," not performing an outer reduction until it has reduced all its subterms.

But this isn't the case. The difference between lazy and eager evaluation is not a difference in evaluation strategy, but rather a difference in the definition of what is reducible. In ordinary evaluation (as opposed to, say, compiler optimizations using partial evaluation), we always use the exact same strategy when reducing terms--typically, always reduce the leftmost, outermost redex. The difference is in the definition of redexes.

In call-by-name lambda calculus, the definition of a reducible expression is an application whose operator is a value. The operand can be any arbitrary expression. As a result, non-values end up being passed as arguments to functions. In call-by-value, we likewise only perform reduction when the operator is a value, but we also require that the operand be a value as well.

The combination of an outermost reduction strategy with the call-by-value rule may appear to be the same as an innermost reduction strategy; after all, it forces the evaluation of subterms before reducing a compound term. But it doesn't force the evaluation of all subterms, specifically, underneath abstractions. This is the key distinction.

Here's an example that distinguishes the three semantics. Imagine an untyped lambda calculus with two effects: we can ask Alice a question, say by sending her computer a message over the network and receiving a response, or we can similarly ask Bob a question. Each of these operations results in a distinct observable effect. Now take the following simple program:

(λx.(ask bob)) (ask alice)

We'll annotate each reduction step with a note recording the side effect it produces, if any, so we can see when the effects happen.

In call-by-name lambda calculus with a leftmost-outermost reduction strategy:

      (λx.(ask bob)) (ask alice)
   -> (ask bob)
b! -> 22

In call-by-value lambda calculus with leftmost-outermost:

      (λx.(ask bob)) (ask alice)
a! -> (λx.(ask bob)) 11
   -> (ask bob)
b! -> 22

And finally, the weirdest of them all, an innermost reduction strategy:

      (λx.(ask bob)) (ask alice)
b! -> (λx.22) (ask alice)
a! -> (λx.22) 44
   -> 22

Intuitively, this program should always ask Bob a question and return its answer. Each of these programs preserves that meaning. But in outermost call-by-value it asks Alice a question first and then ignores it, in an innermost evaluation strategy it asks Alice a question second and then ignores it, and in call-by-name it never asks Alice at all.

I added a couple simple effects to the lambda calculus to demonstrate the idea. But in pure lambda calculus, we can still observe differences between these systems because we can demonstrate side effects through non-termination. An expression that leads to non-termination results in different evaluation behavior of a system when the system makes different decisions about when and whether to evaluate the expression.

Proper tail recursion and space efficiency

I just read through Will Clinger's Proper Tail Recursion and Space Efficiency. I'd been scared of it for a few years because I had the impression it was a very technical and subtle paper. There are perhaps a few subtleties but I actually found it very clear and well-written. Here are some interesting points made in the paper:

1. Proper tail recursion is a property of the asymptotic space complexity of a language's runtime behavior. That is, in improperly tail recursive languages, control can consume unbounded amounts of space for programs that, when run in properly tail recursive languages, only require a constant amount of space.

2. In order to measure the space complexity of a language, you have to measure the entire system, not just, say, the stack. Otherwise, someone could always cheat and hide away its representation of the stack in the heap to make it look like the control is more space-efficient than it really is.

3. But when you measure everything including the heap, you have to deal with the fact that the language doesn't ever explicitly deallocate storage. This means that you have to add garbage collection into your model or else the model always increases its space usage unrealistically.

4. Proper tail recursion is totally natural in the lambda calculus. An application is always replaced by the body of the applied function, regardless of whether it's a tail call. It's just languages with that freaky return construct that accidentally make the mistake of leaving around residue of the application expression until it's completed evaluating. In order to model improper tail calls in Scheme, Will actually has to add a silly return context frame, whose sole purpose is to degrade the space efficiency of the language.

5. By leaving the expression language the same but changing the definition of the runtime system (in this case, the set of context frames), you can compare apples to apples and look at the same space consumption of the exact same program in one system or another, assuming the systems always produce the same results from the programs. Then we can actually construct space complexity classes to classify the different systems.

The Rule of Least Power

Via Phil Wadler's blog, I see that Tim Berners-Lee has written a "W3C Finding" on a principle he terms the rule of least power. The idea is that you should use the least powerful language possible to solve any given problem, in order to achieve the greatest ability to reason about the program statically.

I've talked about this principle before as the balance of expressive power with reasoning power.

In working on the ECMAScript design, I've already seen this issue come up several times, for example with the problems caused by dynamic scoping.

Mom was right...

...hygiene really is important!

It took me hours the other day to catch a bug that came from an unintended variable capture in a macro I'd written.

In a reduction semantics I'm implementing with PLT Redex, I wrote a macro to abstract over certain common patterns in my reduction rules. The macro template introduced a temporary name via a call to the name macro in PLT Redex. I thought name was implemented with a Scheme binding and would therefore be hygienically renamed. This was my mistaken assumption; name is implemented with a quoted symbol.

Then later in a reduction rule, I was using my macro and by chance introducing another variable at the call site with the same name as the temporary variable in the macro definition. This silently caused a capture of the quoted name, with unexpected consequences on the meaning of the reduction rule. In this particular case, it cause the reduction rule not to match when it should.

It took hours to discover that it wasn't a bug in my reduction rule at all, but in the implementation of my macro. Imagine trying to debug this if I hadn't just spent years studying macros and hygiene!

Redex is cool

I hadn't looked at PLT Redex since its pre-publication days, but yesterday I started using it to implement my draft model for Topsl, the programming language for implementing online surveys. I couldn't believe how easy it was! I expected it to take quite a while, but within an hour I had a working operational model of core Scheme, and half an hour later I had the entire grammar of Topsl and even a few nice abstractions. I haven't quite finished the implementation yet, but it's been surprisingly painless.

Of course, it helps to have a good understanding of macrological^* pattern-matching and template instantiation, capture-avoiding substitution, and Felleisen-style context-sensitive reduction semantics, so you might say I'm uniquely suited to use the tool. Regardless, I'm very impressed.

^* This is a very silly adjective. Please don't ever use it. Someone could get hurt.

The call stack is not a history

I had a fascinating conversation with John Clements yesterday about continuation marks, and he gave me a nice way of clarifying a common misconception about the call stack. There are two major pieces of information you might like to inspect about the control flow of a program: what the program has already done (its history), and what it has left to do (its future).

The call stack might appear to be giving you information about the history of the program execution, but in fact, it's an incomplete history. For example, any functions that have already returned are not recorded; they've already popped off the stack. Languages that implement proper tail calls also remove information about function calls that have completed just about everything but may not yet have returned from their tail operations. Now, if this is information you need, it doesn't mean you can't record it through some other means. It just means the default behavior of the runtime is not to record it--and for good reason, too. Not accumulating that information affects the asymptotic space complexity of the runtime. You wouldn't want your runtime collecting complete information about every iteration of a for-loop by default, either, just on the off-chance that information might be useful!

The evaluation context, i.e. call stack, is not about the history of the program execution. It contains a complete record of the remainder of the program execution, the work the program has left to do. That's the whole reason for maintaining stack frames, so that when a function returns, the runtime knows what to do next. So stack inspection is fundamentally about inspecting the future of the computation, not about recording its history.

From the that'll-be-the-day department

On the plt-scheme mailing list, Matthew announces that PLT Scheme now builds on the new macs. Now who ever expected to see statements like the following in this lifetime?

MzScheme passes its test suite. I don't know whether MrEd and DrScheme
actually work, because I've only had console access to an Intel Mac.

Nancy typing

It's popular in scripting languages to perform lots of automatic conversions on data in an attempt to "do what I mean". In some cases, the heuristics for conversion are arguably relatively clear, but sometimes the language is so eager to find some way to make the operation consistent rather than simply give an error (and force the programmer to be more explicit) that extremely bizarre and unpredictable behavior ensues.

I call this Nancy typing, for a delicious reason that will soon become clear. What this has to do with duck typing, I'm not sure--I can't find a straight-forward definition. According to Wikipedia's rather confused entry it's not the same thing as structural types, but the jury seems to be out in this LtU thread. As far as I can tell, duck typing either has something to do with the idea of performing conversions between separate datatypes in order to support an operation or simply subtyping based on the set of supported operations. Actually, in the TAPL chapter on structural types, Pierce points out that structural type systems often include axioms that assert subtyping relationships between types whose runtime representations are completely different (such as float and int, for example), and these coercions actually have to be implemented in the runtime by conversions. So maybe the distinction is artificial, and duck typing really is the same thing as structural subtyping.

Anyway, the typical example used to demonstrate the hazards of structural subtyping is a GraphicalObject class and Cowboy class that both implement draw operations with entirely different meanings. But I prefer the Nancy bug.

My friend Mike MacHenry told me this story. Mike's company has an expert system, written in Perl, that employs heuristics to determine whether a customer is likely to have filled out a form incorrectly. One of the heuristics is supposed to check that the names given in two different columns of a record are the same. Now, it turns out that the comparison was implemented wrong--the software was almost always reporting that the names were the same, even when they weren't--but because the expert system is only making a best guess, this just passed unnoticed for a while as a false negative.

But every once in a while, the system reported a false positive, i.e., that the names were not the same when in fact they were. And it just so happened that in each one of these cases, the name in the record was "Nancy."

The explanation is that the programmer had accidentally used the numeric equality operation, rather than string equality. Perl silently converted the strings to numbers in order to make the operation succeed. Since in most of the cases, the strings were not numeric, Perl parsed the maximum numeric prefix of the string, namely the empty string. It so happens that the empty string happily converts to 0 in Perl, so most of the time, any pair of strings both convert to 0, and the equality comparison evaluates to true.

But "Nan" is parseable in Perl as not-a-number, which is always considered unequal to any number, including itself. So "Nancy" happily converts to not-a-number, and then tests false for numeric equality to itself.

Tada! The Nancy bug.

Update:

JavaScript language level

I've released the first version of my JavaScript language level for DrScheme in PLaneT, the centralized package distribution system for PLT Scheme. To try it out, do the following:

1. Install DrScheme version 30x.
2. Add the binaries directory ($PLTHOME/bin under Unix derivatives and %PLTHOME% under Windows) to your system's PATH.
3. From the command line, run:
   

   planet -i dherman javascript.plt 1 0

4. Now start up DrScheme and select "JavaScript" from the "Choose Language..." menu item.
   

Warning: this rhino may be infested with bugs.

ECMA-262 Edition 4

As Brendan Eich announced yesterday, I've been invited to join Mozilla and ECMA in the process of defining and specifying the next version of JavaScript--erm, EcmaScript. Brendan kindly refers to me as an "expert" (for which I've heard no end of snickers from my colleagues--thanks guys), but I expect to learn a lot from this experience. I just met the Mozilla and ECMA guys last week, and they seem great to work with.

I'm really excited about the marriage of formal methods and practical application. I love to see this kind of cooperation between research and industry. At a minimum, the PL community's knowledge about formal specification should help the committee with its goal of making the spec clear and precise. We are actually hoping to see some correctness proofs as well--e.g., type and contract soundness. And I'm keeping my eyes peeled for other useful consistency properties worth verifying.

Sorry about the silence lately. Now that the word's out, I hope to talk more about some of the interesting points that come up in the EcmaScript process.

Why isn't the clipboard a stack?

For 22 years now, graphical OSes have offered the same puny little single ref-cell as the model of the clipboard, i.e., the storage for the copy-paste mechanism. Yet most of the interaction I have with my computer is stack-shaped; start performing a task, realize it requires a sub-task, perform the sub-task, and return to the previous task. If I happen to have copied something to the clipboard which I am pasting in various places and then need to perform a sub-task in the middle, this single register may become trashed in the process, with a "user-save register policy" as my only recourse.

I know Microsoft Office has some sort of fixed-width-but-bigger-than-1 array for its clipboard, but it's only within Office, not OS-wide.

I'm not saying the design of a stack-based clipboard would be obvious--for example, I don't know how the system should know when to pop an item off the stack--but a single ref cell isn't enough.

Work in progress

Three productivity boosters

A few of my current favorite productivity boosters:

1. Subversion - With CVS, I wasted a lot of time fretting about file names and directory structures, because it was such a pain having to muck with the repository when I changed my mind. I ended up not being able to prototype nearly as rapidly because I spent time trying to plan the overall structure of my code. Sometimes I'd even give up and go off to work on something else. With Subversion I just blithely give things whatever name and directory structure suits me at the moment and keep working.
2. Voo2do - This is the best task-list and project management software I've found online so far. It's got the right features and no more: I can give tasks a name, an associated project, and optionally a priority, a deadline, and notes; then I can create custom views over a particular set of projects. And that's about it. Now I'm keeping all of my to-do lists for everything in one place. Since I've been in grad school, I've found I do a lot of task-switching between my various jobs, so being able to keep all my tasks listed in one place should help me maintain my priorities not just in the context of one job but amongst all of them.
3. Procmail - You've just gotta keep separate folders for emails from separate projects.

The name of the game appears to be unobtrusiveness of the technology (K.I.S.S.), a high payoff-to-learning-curve ratio, and the ability to reorganize continuously.

I'm still on the lookout for good calendar software. Ideally online and compatible with Apple iCal.

Expressions and statements

This post explaining the I/O monad to a newbie on the Haskell mailing list motivates it in terms of expressions and statements:

We have a[n] "evaluation machine" and a[n] "execution machine". The former
evaluates expressions, the latter executes I/O actions. When the program is
started, the execution machine wants to execute the actions from the "main to
do list".

Interesting. Imperative languages like C distinguish expressions and statements syntactically, but with various implicit conversions between them, e.g., expression-statements and procedures that execute statements but then return values. Haskell separates statements from expressions with the type system, and keeps them apart more strictly (no pun intended). But in a sense they're both making the same distinction.

I dare you

Read these three posts about Real's business practices and try not to get angry.

12 Weeks With Geeks

This looks interesting:

http://www.projectaardvark.com/movie/

It features some of your favorite outspoken software evangelists, Joel Spolsky and Paul Graham.

I'm not sure what I'll think of it, because on the one hand they're billing it as a more honest look into the software development process, which should be informative, but on the other hand, the preview hints at a number of the myths computer people like to believe about themselves.

I find myself increasingly upset at the way people in software are portrayed both by the media and by themselves--as idiot savants, socially inept geniuses, lone ranger superheroes, and revenge-of-the-nerds underdogs. It's dangerously delusional, it fosters extreme anti-social behavior, allows for all sorts of irresponsibility and incredibly bad software, continually dissuades women from entering the field, and perpetuates the belief that each hacker can solve any problem alone with complete disregard and disdain for a century of progress and collective knowledge.

How long can we continue duping the world into relying on us to design the heart of every automated mechanism known to man? How long will people continue believing in the myth of the 15-year-old hacker genius while simultaneously decrying the unreliability of software before the cognitive dissonance finally cracks?

At any rate, I don't know if that's where this movie is going. You can only tell so much from a preview. But it should be very interesting, especially about the product lifecycle and management perspectives.

Try-catch-finally in Scheme

I need a little break from all this parsing crap. Let's have some macro fun. Here's a PLT Scheme version of Java's try-catch-finally. Note the use of symbolic literals, rather than the usual syntax-rules/syntax-case literals list. This is due to my philosophy on macro keywords.

(define-for-syntax (symbolic-identifier=? id1 id2)
  (eq? (syntax-object->datum id1)
       (syntax-object->datum id2)))
  
(define-syntax (try stx)
  (syntax-case* stx (catch finally) symbolic-identifier=?
    [(_ e (catch ([pred handler] ...)) (finally e0 e1 ...))
     #'(dynamic-wind void
                     (lambda ()
                       (with-handlers ([pred handler] ...)
                         e))
                     (lambda () e0 e1 ...))]
    [(_ e (catch ([pred handler] ...)))
     #'(with-handlers ([pred handler] ...) e)]
    [(_ e (finally e0 e1 ...))
     #'(dynamic-wind void
                     (lambda () e)
                     (lambda () e0 e1 ...))]))

Example use:

(try (begin (printf "hi")
            (printf " there")
            (printf ", world")
            (newline)
            (error 'blah))
  (catch ([exn? (lambda (exn) 3)]))
  (finally (printf "finally!~n")))

Dynamic scope

Now I'm confused by another aspect of JavaScript scope:

var f = function() { alert("default") }
function test(b) {
    if (b) {
        function f() { alert("shadowed") }
    }
    f()
}

Evaluate test(true), and you'll see "shadowed". Evaluate test(false), and you'll see "default". Apparently function declarations are another instance where JavaScript is not lexically scoped (in addition to this, arguments, and the behavior of references to unbound variables).

Update: Oh, I forgot to mention the with construct -- another instance of dynamic scope.

Update: Also note that this is not the same thing as the behavior of var. If we write this function instead:

var f = function() { alert("default") };
function test(b) {
    if (b) {
        var f = function() { alert("overridden") };
    }
    f()
}

Then with test(true) we still get "overridden", but with test(false) we get an error from trying to apply undefined as a function. In other words, in this example, we have normal lexical scope with hoisting.

Update: I think this settles it--it's pretty much what it looks like. In chapter 13 of ECMA-262, the dynamic semantics of a FunctionDeclaration is to create a new binding in the "variable object" (ECMA-262 terminology for an environment frame) upon evaluation of the declaration.

If you imagine an environment as a list of frames, then in a lexically scoped language, this is a statically computable list. In a language with dynamic scope, frames in the environment may be generated or mutated at runtime, so it's not statically computable. JavaScript has some of both, so there are some things you can know statically about a variable reference, and some things you can't.

Update: The saga continues... I realized that I couldn't actually derive the above example from the official ECMAScript grammar! I see that others have made this surprising discovery as well: you can't nest FunctionDeclarations beneath Statements. Furthermore, you can't begin an ExpressionStatement with a FunctionExpression. As a result, it's impossible to derive the above program.

However, in practice, JavaScript engines do appear to accept the program, and use the dynamic semantics from chapter 13 as I describe above. But for strict ECMAScript, I can't seem to produce an example. I thought I could still force the issue by placing the nested function at the top-level of the enclosing function body and conditionally returning. But I was thwarted by two more interesting phenomena. First of all, when a var declaration and a function declaration compete to bind the same identifier, the var always wins, apparently. So this always produces "default", regardless of the value of b:

function test(b) {
    var f = function() { alert("default") };
    if (!b) {
        f();
        return;
    }
    function f() { alert("overridden") }
    f()
}

Second, nested function declarations appear to be hoisted to the top of the function body. So the following example always produces "overridden":

var f = function() { alert("default") };
function test3(b) {
    if (!b) {
        f();
        return;
    }
    function f() { alert("overridden") }
    f()
}

Curious. At any rate, the behavior of popular JavaScript engines (Firefox and Rhino) seem to be a generalization of ECMAScript (by allowing FunctionDeclarations to appear nested within Statements) that is consistent with the spec (by obeying the behavior specified by section 13).

Now I need to confirm these two more properties of the language with the spec.

Gotcha gotcha

In "a huge gotcha with Javascript closures," Keith Lea describes an example function written in JavaScript with surprising behavior. But he misattributes the unexpected results to the language spec's discussion of "joining closures." The real culprit, rather, is JavaScript's rules for variable scope. Let me explain.

Here's Keith's example:

function loadme() {
 var arr = ["a", "b", "c"];
 var fs = [];
 for (var i in arr) {
   var x = arr[i];
   var f = function() { alert(x) };
   f();
   fs.push(f);
 }
 for (var j in fs) {
   fs[j]();
 }
}

We might expect the function to produce "a", "b", "c", "a", "b", "c", but surprisingly, it displays "a", "b", "c", "c", "c", "c"! Wha' happened?

The answer is that, in JavaScript, all var declarations are hoisted to the top of the nearest enclosing function definition. So while x appears to be local to the for-loop, it is in fact allocated once at the top of the loadme function and in scope throughout the function body. In other words, the above function is equivalent to:

function loadme() {
 var x;
 var arr = ["a", "b", "c"];
 var fs = [];
 for (var i in arr) {
   x = arr[i];
   var f = function() { alert(x) };
   f();
   fs.push(f);
 }
 for (var j in fs) {
   fs[j]();
 }
}

In this version, it's clear why the function behaves as it does: the closure is mutating a global variable every time it's called!

To get the desired behavior, you need to use nested functions instead of loops, e.g.:

function loadme() {
 var arr = ["a", "b", "c"]
 var fs = [];
 (function loop(i) {
   if (i < arr.length) {
     var x = arr[i];
     var f = function() { alert(x) };
     f();
     fs.push(f);
     loop(i + 1);
   }
 })(0);
 for (var j in fs) {
   fs[j]();
 }
}

Now x is truly local to the loop body, and the function produces "a", "b", "c", "a", "b", "c" as expected.

Update: My suggested fix is really bad advice for ECMAScript Edition 3! I should never recommend using tail recursion in a language that is not properly tail recursive. If all goes according to plan for proper tail calls in Edition 4, my suggestion would be fine for that language. But today, you can't use tail recursion. Instead, you should use any of the existing lexical scope mechanisms in ECMAScript for binding another variable to the loop variable i.

Solution 1 - wrap the closure in another closure that gets immediately applied:

function loadme() {
  var arr = ["a", "b", "c"];
  var fs = [];
  for (var i in arr) {
    var x = arr[i];
    var f = (function() {
                 var y = x;
                 return function() { alert(y) }
             })();
    f();
    fs.push(f);
  }
  for (var j in fs) {
    fs[j]();
  }
}

Solution 2 - wrap the loop body in a closure that gets immediately applied (suggested in the comments by Lars):

function loadme() {
  var arr = ["a", "b", "c"];
  var fs = [];
  for (var i in arr) {
    (function(i) {
        var x = arr[i];
        var f = function() { alert(x) };
        f();
        fs.push(f);
     })(i);
  }
  for (var j in fs) {
    fs[j]();
  }
}

Solution 3 - wrap the closure in a let-binding (in JavaScript 1.7, currently implemented only in Firefox 2):

function loadme() {
  var arr = ["a", "b", "c"];
  var fs = [];
  for (var i in arr) {
    var x = arr[i];
    var f = let (y = x) function() { alert(y) };
    f();
    fs.push(f);
  }
  for (var j in fs) {
    fs[j]();
  }
}

Solution 4 - ditch var entirely and only use let (again, currently specific to Firefox 2):

function loadme() {
  let arr = ["a", "b", "c"];
  let fs = [];
  for (let i in arr) {
    let x = arr[i];
    let f = function() { alert(x) };
    f();
    fs.push(f);
  }
  for (let j in fs) {
    fs[j]();
  }
}

The moral of the story is that in ECMAScript Edition 4, let is a "better var", behaving more like you'd expect. But until you can rely on let as a cross-browser feature, you'll have to use solutions like 1 and 2.

Semanticist's cookbook

Is this a dumb idea? I'd like to create a semantic modeling wiki where people can describe various techniques for modeling different kinds of programs, programming languages, and programming language features mathematically. Sort of a clearinghouse or cookbook for semantics. It could feature links to literature, and various categorizations so that people could find recipes by following different paths. For example, a reader might discover the exception monad by alternatively searching for control features, or error handling, or denotational modeling, or monads, etc.

Perhaps a better-designed database would be more organized, but I think wikis are good for continuously reorganizing, as well as for community contribution.

The Semanticist's Cookbook. I like it!

Update: Stubbed at http://semanticscookbook.org.

Update: Maybe I'll install a wiki another time but I don't have time for this now.

What makes a good paper?

Or: Theorems are the test cases of semantics

Good PL papers define their systems with enough greek symbols, funky operators, inference rules and the like (what Mitch calls "dirty pictures") to demonstrate depth and precision of intellectual content. Without proving subsequent theorems based on these systems, though, there's no evidence that these systems are actually consistent or even useful.

A programming language semantics is, as Mitch puts it, "a mathematical model for predicting the behavior of physical systems." One of its primary purposes is reasoning (at a particular level of abstraction) about programs written in that language. It's generally hard to prove that a semantics is "the right one" for the problem space, which is a fuzzy notion, but theorems raise its probability of being useful.

A semantics alone may at least convey information about a language, since math is often more concise and precise than English. But without being put into use, it's doubtful whether it is really a specification; it's far too easy to slip into specifics as an algorithm. Or at the other extreme, it may leave out too many details to address the salient issues in the problem space. And who knows what subtle errors are lurking within the language definition? The best way to ensure that a semantics accurately defines a language at an appropriate level of abstraction is to prove theorems with it.

Delicious dudgeon

From Joel.

Values in Non-Strict Languages

In the literature on non-strict languages, the term "value" seems to be used in a different way. In call-by-value languages, we classify a set of normal forms that we define as the "values" of the language, and arguments to functions must evaluate to values before the functions can be applied. But because in call-by-name or call-by-need languages, you can pass arbitrary, unevaluated expressions to functions, the notion of a value is in a sense less critical. You still need to define the normal forms in order to determine when to stop evaluating the whole program (or when to stop evaluating arguments to primitives with strict positions). But interestingly, in The Implementation of Functional Programming Languages, Peyton Jones still refers to the expression that a function argument is bound to as the variable's "value" -- despite the fact that it may not be in weak head normal form. Apparently the term "value" is informally used to mean a variable's binding, whereas the final result of an evaluation is only referred to as a normal form.

A packrat parser for Scheme

Through some random poking around the web, I just discovered this packrat parser in R5RS Scheme. I need to check that out.

Update: That's a parser in Scheme, not a parser for Scheme. (Thanks, Mitch.)

Update²: Not entirely random, Noel, thanks. Though discovering Tony's files by URL munging certainly was random.

Language that represent themselves

In studying macros, I've discovered a fundamental complexity in one axis of language design: making aspects of a language easily representable within itself hampers the plasticity of the language. That is, as soon as you make it easy to observe the internals of the language, any changes you make to the language become by definition observable. As a result, any time you add, remove, or change a language feature, you add must consider that feature's representation within the language and how it affects the semantics.

This is well known to designers of languages with reflection, and causes all sorts of ulcers for compiler writers. But it's also a pain for designers of macros. For example, every time you add a new type of expression to the language, macros must be able to consume and produce that type of expression. Scheme makes this easier by generally having just one kind of expression--but in reality, that's a lie! Definitions are different from expressions, and cause lots of subtle complexities.

Contracts fall right out

Jacob Matthews came to town this past weekend for several events, and on Monday gave a fabulous talk at Northeastern on multi-language systems. The experience made me proud to be a member of both the Northeastern PRL and the PLT research family. Jacob's work looks like it could be very useful, and I hope to apply it to several of my research projects. And the presentation was fantastic: he was entertaining and charismatic, and our group was a lively and interactive audience.

He's been talking for some time about how when programs interact between typed and untyped languages, "contracts fall right out." I was looking forward to finding out how, and he kept telling me that once I saw it it would be obvious. It had sounded rather magical to me, but sure enough, about halfway through his talk it became totally obvious! If a typed language is to use an expression from an untyped language in any useful way, it'll have to have a dynamic check to make sure the expression really was of the right type. But of course, you can't in general dynamically check the type of a procedure, so contracts are a natural solution!

Don't evaluate under lambda

In the past, I've been unsure what Alan Kay meant whenever he talked about "late binding" being the key insight into the development of Smalltalk, an insight which he attributes to his reading of the Lisp 1.5 manual. I think what he's talking about is the idea that if you have some part of your program that contains a piece of data, but now you want the construction of that data to vary based on some particular condition of the dynamic execution of the program, wrap it in a procedure. Now you can dynamically generate the data instead of fixing it once and for all.

This is of course possible regardless of whether you're in an OO or FP framework; in the context of OO, he's referring to the idea that instead of a record with fixed fields, you use methods that dynamically return the values of the fields. In functional languages you can do the analogous thing by placing functions in the slots of records, or in general you can just replace any datatype α with (→ α).

You can also take this in arguably the wrong direction and base the dynamic generation of this data on the mutable state of the program (whether that's the mutable fields of the object the method belongs to, or the mutable state of variables in the closure of a procedure). So you can see how late binding could be seen as a gateway drug to overuse of mutation.

But more and more I appreciate the power and simplicity of this notion that the natural path a program follows as it gets more complex is to take the pieces that are fixed and abstract them; to take the constants and make them variable; to take variables and fields and turn them into procedures and methods.

Post-Redirect-Get with the PLT web server

Here's a nice idiom easily expressed with the PLT servlet library. Typically in an interactive web application you'd like to respond to form submissions (via "POST") with a page that the user can safely refresh, i.e., a page delivered via "GET". As a result, most people recommend you use what's known as the "Post-Redirect-Get pattern," where the immediate response to a POST is a redirect to an ordinary GET page.

Look how beautifully this is expressed in PLT Scheme:

(define (redirect/get)
  (send/suspend
    (lambda (k-url)
      (redirect-to k-url))))

The send/suspend procedure reifies the current continuation as a web continuation URL. The redirect-to procedure generates a response that redirects the user's browser to the given URL. By combining the two, we simply redirect the user's browser right back to exactly the point in the computation where we are, the only difference being that we've now returned from a "GET" interaction instead of a "POST". Usage looks like:

(define (start initial-request)
  (let ([request (send/suspend
                   (lambda (k-url)
                     ... form ...))])
    (redirect/get)
    (let ([user (extract-binding/single
                  'user
                  (request-bindings request))])
      `(html (head (title "Hi"))
             (body (p "Hi, " ,user "! Hit refresh!"))))))

(Added to the Scheme Cookbook.)

One-step reduction semantics a historical mistake?

Wow, I just discovered this thread where Thorsten Altenkirch declares small-step operational semantics a "historical mistake." Sometimes I forget how specific the research culture I'm a part of is; given how often I use small-step semantics and abstract machines, I just assume that's what everyone does. But there are many people who consider big-step semantics to be more "natural." (Whatever that means.)

What confuses me about the popularity of big-step semantics in the typed functional language community is that Matthias's approach to proving type soundness via subject reduction in a small-step operational semantics is by now the de facto standard technique.

Anyway, I honestly have no idea how you'd reason about non-trivial language features like continuations with a big-step semantics.

How do we automate?

Read this excellent and reasonable post from Jacob Matthews on undergraduate curriculum in computer science.

Let me call attention to Jacob's characterization of CS: "computer science is fundamentally the study of how to best systematically solve problems." I think it's interesting to compare this to Knuth's definition of computer science (pp. 5-6) as the answer to Forsythe's question "what can be automated?" (With some quick googling I found a slight generalization of this formulation to the broader question "how do we automate?")

It's useful to place Jacob's definition in the context of our research culture. You could describe us as belonging to the academic diaspora of Matthias Felleisen, whose profound textbook How to Design Programs and corresponding pedagogy permeate our approach to computer science. (The book's title is an homage to Polya's How to Solve It, a landmark work in the history of mathematical pedagogy, which sought to elevate math education beyond the realm of black art by providing students with a systematic process for solving problems rigorously.) The HtDP approach to teaching computer science is to give students a repeatable process for solving problems--this is systematic both in the sense that students are given a dependable process that they can reliably use to solve new problems, and in the sense that expressing the solution in terms that a computer can execute and evaluate is more formal and reliable than a rote hand-calculation.

Nevertheless, I like Knuth's and Raatikainen's definitions. Computer science is not always about problems--both in research and industry, I think there's a place for exploration where the discovery of applications may not follow until later. The real common thread seems to be the ability to describe any process in a formal way so that it can be specified without unnecessary implementation detail and yet in a way that it can be repeated reliably.

The language in my head

Felix points out how bizarre the hypothetical language was that I used in my previous post. Very true! It combines Javascript object-literal notation, ML expression syntax, semantic brackets to represent compilation, Scheme's hygienic expansion, Java (et al) method invocation, and hey, let's give credit to the new guy, Fortress-style mathematical notation for set-union.

Well, I know what I like!

Compiling a language with multiple operations

I've now twice compiled languages with more than just an eval operation on expressions. For example, I wrote an LL(1) parser generator that generated for each expression in the grammar an object with a parse method (which you can think of as eval for grammars) as well as first, follow, and nullable? methods. I've also run into the same issue when working on the Topsl compiler.

But when you generate objects for expressions and you need to model binding in your language, you find an interesting little problem. Imagine compiling a simple functional language into a bunch of expression objects that have two methods: eval and analyze (for some hypothetical static analysis you might like to perform). Now how would you implement the rule for compiling let-expressions?

[[let x = e1 in e2]] =
    { analyze : λ().[[e1]].analyze() ∪ let x = ()
                                           in [[e2]].analyze(),
      eval : λ().let x = [[e1]].eval() in [[e2]].eval() }

By binding the variable x in both methods, it can be referred to in the compiled code for e2. In the static analysis, we can bind it to any dummy value, since the analysis presumably doesn't care about the dynamic result of evaluating the expression.

But this results in duplicating the expansion of e1 and e2, which is not just code bloat, it's exponential code bloat. A non-starter.

We could then lift out the generated let to surround the entire object creation, initialize x to a dummy value, and then mutate it within the body of eval. But this introduces brittle dependencies on the order in which the methods can be invoked.

Instead, we can generate one piece of code, specifically, a function from x-value to expression object, and then invoke this function differently from each method:

[[let x = e1 in e2]] =
    let f = λx.[[e2]]
    in { analyze : λ().[[e1]].analyze() ∪ (f ()).analyze(),
         eval : λ().(f [[e1]].eval()).eval() }

Now there are no fragile method invocation interdependencies, and each method can give a different value for x, and each expression is only compiled once.

Update: I wasn't clear that the semantic brackets function [[--]] represents Scheme-style macro-expansion. So I assume all hygiene issues are handled automatically by the expansion process.

Meta-lambda

Here's something that used to bother me when reading Winskel and learning denotational semantics.

We start with a language like the lambda calculus, and everyone looks at λn.(n+1) and knows that this represents the function that takes an integer and increments it. But that's not enough for us: we have to build up this big, complicated mathematical machinery to determine precisely what this function means; we treat it as dumb syntax and give it a translation to some domain that models it.

But when we're defining the model, we allow ourselves to represent meta-functions simply using the lambda calculus, and suddenly λn.(n+1) just means the set-theoretic function that maps integers to their successors. Why do we have to work so hard to give a precise model for our object language, but when we work with the meta-language, we can just say "you know what I mean"?

The reason is simply that the object language is generally a complex language that's made to look like lambda calculus, but has other features and effects (e.g., recursion and non-termination, mutation, etc.) that can't be modelled in obvious ways and require a precise translation. By contrast, when we work in the model, if it's simply set-theoretic functions, then we can use a simple meta-language based on the lambda calculus to represent these functions. So this meta-lambda calculus is just a convenient shorthand for elements in the domains of the model. As long as there's an obvious translation of such representations into sets, terms in the meta-lambda calculus such as λn.(n+1) can be treated as nothing more than a convenient notation, no different from { (n, n+1) | n ∈ N }.

Pointed domains

In a denotational semantics for a language with non-termination, you use pointed domains, i.e., CPO's with a bottom element. But some of the usual constructions on compound domains such as pairs and sums end up combining multiple bottom elements into one domain. Because the existence of a bottom element is used for the proof of the existence of fixpoints for all functions, it's critical that every domain have a single bottom element. So that's what the "coalesced sum" and "smash product" constructions are for: they identify multiple bottom elements in multiple domains into a single bottom element in the combined domain. [Abramsky and Jung 94, 3.2]

Trust me

I don't understand how you can get away with leaving out proofs in a publication. Given the constraints on the length of the paper, I could imagine providing external references to more complete proofs, say in a companion technical report. It's one thing to trust provided proofs, when even then they are error-prone. But how can you believe a theorem stated without even any indication of a proof? That's kind of the point of math.

I'm reading a couple of papers on FreshML and FreshO'Caml, and they're great work. But the ICFP paper from 2003 has a number of unproved theorems, and then they posted an erratum stating that one of their theorems is flawed, but they haven't bothered fixing it because they have a new paper that takes a different approach. This kind of thing makes me generally nervous about the reliability of research and publications.

Reasonable Defaults

I went to add a mail filter rule to Apple Mail in Tiger, and the new rule came up with a default rule for filtering messages where "Any Recipient" matched the recipient of the current message I was looking at. Beautiful! It gets better -- I went to add another condition, which I changed to a "From" condition, and it automatically changed the initial value of the condition to match the sender of the current message. I never had to type in a single value, switch window panes, copy or paste.

This is something library and language designers could learn from HCI--making the common cases easy. (The Perl-mongers know it.) It's up there with progressive disclosure.

alphaCaml

I've written my first Cαml program: a little lambda-calculus term manipulation language and interpreter. Since it's a language for manipulating terms, there's an object language (the lambda calculus) and a meta-language (the term manipulation language). Expressions in the meta-language evaluate to lambda calculus terms; for example, cps e evaluates the expression e to get a term and then converts the term to continuation-passing style.

Here's the data definition and binding specification of the object language datatype:

sort var
 
type term =
   | Var of atom var
   | Lam of < lambda >
   | App of term * term
 
type lambda binds var = atom var * inner term

The declaration sort var declares a disjoint universe of atoms that will be used as lambda calculus variables. The type lambda is a binding datatype: it binds atoms of sort var, which are then in scope in the right-hand conjunct of the product type (the keyword inner indicates that all the bindings in lambda are in scope in the term). This binding specification actually automatically generates a bunch of Ocaml datatype and library definitions, including:

type term =
   | Var of var
   | Lam of opaque_lambda
   | App of term * term
 and var = Var.Atom.t
 and lambda = var * expression
 and opaque_lambda

val create_lambda : lambda → opaque_lambda
val open_lambda : opaque_lambda → lambda

By making the contents of the Lam constructor opaque, it forces programmers to use open_lambda whenever they need to get at its contents, which has the side effect of freshening all of its bound names. This alleviates the programmer from having to avoid capture explicitly, since bound names are kept unique.

Now here's a term manipulation function written in Cαml. (In fact, this is really just an Ocaml program, since the only extension to Ocaml is the binding specification language. Beyond that, Cαml is just a library.)

let make_lambda : var → term → term = fun v body →
  Lam (create_lambda (v, body))
 
let rec beta : term → var → term → term = fun t x arg →
  match t with
  | Var x' when Var.Atom.equal x x' → arg
  | Var _ → t
  | App (l, r) → App (beta l x arg, beta r x arg)
  | Lam lam → let (x', body) = open_lambda lam in
                make_lambda x' (beta body x arg)

let rec reduce : term → term = function
  | App ((Lam lam), rand) when isValue rand →
      let (x, body) = open_lambda lam in
        beta body x rand
  | App(rator, rand) when (isValue rator) && (isValue rand) →
      raise No_redex
  | App(rator, rand) when (isValue rator) →
      App(rator, reduce rand)
  | App(rator, rand) →
      App(reduce rator, rand)
  | _ → raise No_redex

There's no need to implement capture-avoiding substitution, because every time an abstraction is opened, its bound variable is automatically freshened by open_lambda.

Stupid keywords

I spent like 20 minutes trying to figure out what I was doing wrong with the syntax of pattern matching in Ocaml, only to discover the problem wasn't with pattern matching at all: I was trying to bind the name val, which is a keyword in ML:

let (key, val) = List.find( ... )

Learning a new language is such a pain. I thought I'd grown out of stupid problems like this. You almost can't blame developers for resisting learning new technologies.

Subtleties of getElementsBySelector

I should point out that my implementation of getElementsBySelector corrects a couple of subtle bugs in the original version. For one thing, the original version searches for nodes of the form #foo by using document.getElementById; this results in finding the outermost node in the entire document whose ID matches, even if searching a subtree. Since ID's are not guaranteed to be unique, this can produce the wrong node.

An even more subtle bug in the original version is that multiple copies of the same node may appear in the result array. For example, the selector '.foo .bar .mumble', when applied to the following tree:

<div class="foo">
    <div class="bar">
        <div class="bar">
            <div class="mumble">mumble</div>
        </div>
    </div>
</div>

...produces two copies of the mumble node, because it finds it by following two different paths. By contrast, my implementation visits each node in the entire document tree exactly once, so it is guaranteed to produce either 0 or 1 copy of each node in the result array.