Wednesday, June 28, 2006

Backwards compatibility

One of the biggest lessons I've learned from the ECMA process is how critical backwards compatibility is. When you have millions of users, the enormous weight of existing software holds you back from doing just about anything that breaks compatibility. An email from Brendan on the ES4 public mailing list (you have to subscribe to the mailing list to view the original email) crystallizes the difference:
...we are not breaking backward compatibility except in selected and few ways that actually improve the bugscape.
In other words, if you expect that a break in compatibility will cause fewer bugs than it fixes, then it's acceptable.

Wednesday, June 21, 2006

A semantics for prophecies

Here's a quick sketch of a semantics for prophecies. Let's model a multi-threaded mini-Scheme where thread interleaving is represented by non-deterministically choosing a thread from a list of active threads and reducing it one step:
(e1, ..., E[e], e2, ...) → (e1, ..., E[e'], e2, ...)
We also need a store to represent creating and updating prophecy queues. So the rule for cleaning up a terminated thread looks like:
<(e1, ..., v, e2, ...), σ>
    → <(e1, ..., e2, ...), σ>
And beta-reduction occurs in a thread like so:
<(e1, ..., E[((lambda (x) e) v)], e2, ...), σ>
    → <(e1, ..., E[e[v/x]], e2, ...), σ>
Creating a new prophecy causes a new thread to be spawned and allocates a new, empty queue on the store. The prophecy's thread marks its context with the location of the queue so that subsequent calls to yield will know where to store their values.
<(e1, ..., E[(prophecy e)], e2, ...), σ>
    → <(e1, ..., E[<prophecy: i>], e2, ..., e'), σ[i := <queue:>]>
    where e' = (prophecy-context i e)
When yielding a value, we look up the current thread's prophecy context to find its associated queue, and add the value to the queue. (Because this is an atomic step, queue updates are thread-safe.)
<(e1, ..., E[(yield v)], e2, ...), σ>
    → <(e1, ..., E[null], e2, ...), σ[i := <queue: v1, ..., vn, v>]>
    where E = (prophecy-context E0)
    and σ[i] = <queue: v1, ..., vn>
Finally, reading a prophecy off the queue succeeds whenever the queue is non-empty.
<(e1, ..., E[(prophecy-next <prophecy: i>)], e2, ...), σ>
    → <(e1, ..., E[v1], e2, ...), σ[i := <queue: v2, ..., vn>]>
    where E ≠ (prophecy-context i E0)
    and σ[i] = <queue: v1, v2, ..., vn>
Conspicuously missing from this first draft: the stop-iteration exception (because I didn't feel like adding exceptions to the model), and prophecy->stream, which really can be considered a library function added on top, implementable in a language with delay and force by means of a recursive function that produces null when it catches the stop-iteration exception.

The prophecy was unclear

My explanation of prophecies wasn't very clear. Ezra Cooper asked in the comments:
You say that the subexprs of the prophecy form are evaluated in a separate thread; is each one evaluated in its own separate thread? Or is one background thread generated for that whole prophecy? What happens after yielding--it queues up a value for other threads, but what does the present thread do?
The idea is that a prophecy form spawns one single background thread, which immediately goes to work evaluating the prophecy's subexpressions sequentially. Within that thread, each call to yield queues up its value and the thread immediately continues evaluating (this is in contrast to generators, which cause a transfer of control upon a yield).

When any other thread requests a value from the prophecy, it either dequeues the first yielded value, blocks if no values have yet been queued, or raises a stop-iteration exception if the prophecy is complete (i.e., the prophecy background thread has terminated and all yielded values have been dequeue).

But in my servlet example, each page in the servlet only wants to read one single yielded value, so there's no need to block the page from loading until all the values have been yielded. That's why the prophecy->stream library function provides a lazy stream view of the prophecy which the servlet can use to pull items off the queue by need. That is:
(define (view stream)
(if (null? (force stream))
;; produce a web page signalling that we're done
'(html (body "DONE"))
;; produce a web page displaying the first item in the stream
(send/suspend/dispatch
(lambda (proc->url)
`(html
(body
(p ,(render-item (car (force stream))))
;; a link to view the next item in the stream
(p ,(a ([href ,(proc->url
(lambda (request)
(view (cdr (force stream)))))])
"Next"))))))))
This procedure generates a web page that shows a view over the first item in the stream, with a link to display the next. When the user goes back to the previous page and reclicks the link, the servlet simply reloads this same stream (which was the cdr of the previous page's stream). In other words, we've effectively masked out any mutation. The streams provide a lazy view of an immutable sequence of values, but which are produced "eagerly" in a background thread by the prophecy.

Tuesday, June 20, 2006

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.

Wednesday, June 14, 2006

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.

Tuesday, May 30, 2006

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.

Friday, May 26, 2006

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

Tuesday, May 23, 2006

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.

Friday, May 19, 2006

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.

Wednesday, May 17, 2006

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.

Thursday, May 04, 2006

Lightweight

One possible definition: avoiding unnecessary abstraction.

Friday, April 28, 2006

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:
λyx.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.

Thursday, April 27, 2006

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.

Thursday, April 13, 2006

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.

Tuesday, April 04, 2006

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.

Tuesday, March 28, 2006

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