Even may not be odd after all

Yesterday I complained that even streams can lead to unenforced dependencies between computations. In fact, I think there isn't a problem, at least in the usual implementation strategy. As long as you implement a non-empty stream as a promise of a pair, rather than a pair of promises (or a promise of a pair of promises), you can guarantee the right order of evaluation.

Let me actually test my point this time. First we need an effectful stream computation:

(define (make-reader in)
  (stream-delay
   (let ([first (read in)])
     (if (eof-object? first)
         stream-null
         (stream-cons first (make-reader in))))))

This function creates a stream by reading from an input port, so the order in which its cells are computed is significant. Now here are two different implementations of stream-map:

(define (stream-map1 proc str)
  (stream-delay
   (if (stream-null? str)
       stream-null
       (stream-cons (proc (stream-car str))
                    (stream-map1 proc (stream-cdr str))))))

(define (stream-map2 proc str)
  (stream-delay
   (if (stream-null? str)
       stream-null
       (let ([rest (stream-map2 proc (stream-cdr str))])
         (stream-cons (proc (stream-car str)) rest)))))

The second implementation forces the tail of the list before the head. When I tried these both in PLT Scheme, they evaluated the same:

> (stream→list
   (stream-map1 add1 (make-reader
                      (open-input-string "0 1 2 3 4"))))
(1 2 3 4 5)
> (stream→list
   (stream-map2 add1 (make-reader
                      (open-input-string "0 1 2 3 4"))))
(1 2 3 4 5)

There you have it: the SRFI 40 implementation of even streams (at least the reference implementation and PLT Scheme implementation) doesn't exhibit a sensitivity to the order of observation of elements of a lazy pair.

Now, to make this falsifiable, I should demonstrate a broken implementation of even streams, to watch the same test fail. Uh... exercise for the reader.

Even can be odd

Wadler et al's criticism of the "odd" style of laziness is that it forces some unnecessary (and possibly unwanted) computation. Because only the tail of a stream is delayed, a stream-valued function always computes the head eagerly, even when it isn't needed. They show an example like the following, where taking a prefix of a stream still ends up computing too much because take can't prevent stream-map from computing the first element of the unwanted suffix:

...
→ E[(take 0 (stream-map div (countdown 0)))]
→ E[(take 0 (cons (div 0)
                  (delay
                   (stream-map div (countdown -1)))))]
→ error: division by zero

Their point is well-taken: languages like Haskell have a clearer model of need, and the SICP style of semi-lazy lists is, well, a bit odd.

But today Richard Cobbe warned me of an important subtlety with the authors' proposed "even" streams. Making streams fully lazy, so that neither the head nor the tail is forced unless it is observed, effectively removes any enforcement of order between their computations. In a pure functional language like Haskell, this is fine, but if your stream abstraction is built on top of, say, file I/O, it's all too easy to perform a simple refactoring like lifting a recursion into a let-bound variable:

(define (f str)
  ... (let ([rest (f (stream-cdr str))])
        ... (stream-car str) ... rest ...))

and suddenly you'll find your result stream is backwards, or even permuted!

I'm actually surprised the monadologists in question didn't address this (I've only skimmed the paper, so maybe I missed it). Monads add strictness to a non-strict language to pave the way for side effects, so naturally adding non-strictness to a strict language that already had side effects is going to be tricky.

I don't have any great categorical magic tricks to offer as a solution. But I imagine you could enforce the dependency by brute force: use even streams, except implement stream-cdr in such a way that it first forces the evaluation of the head.

Now I need to read SRFI-45 to understand the subtleties of tail-safe lazy computation, and then maybe I'll finally start feeling comfortable writing stream abstractions in Scheme. I really want to use streams: they make excellent abstractions of many I/O patterns. But they are fiendishly subtle.

Unknown unknowns

I'm always pretty offended by people who intend to become programmers by taking a 1-week course on Java or reading a "Teach Yourself" tutorial. Here's Peter Norvig's advice on the topic. The more you know about programming, the more you become aware of your own limitations. People who think they can "pick up" programming quickly are blissfully ignorant of the vastness of their ignorance. I guess that's probably true of most skills.

Meta-mathematical reasoning

It's common in programming languages to write proofs about proofs. For example, when using a Gentzen-style deduction system for specifying a type system or a big-step operational semantics, we often write a proof by induction on the size of the proof tree of a derivation.

When proving type soundness, you can use a number of different dynamic semantics. It's sanest to attempt this with an operational semantics, but there are many flavors to choose from: big-step operational semantics, small-step semantics with compatibility rules for lifting the basic reductions into arbitrary evaluation contexts, small-step semantics with Gentzen-style rules for creating an inductive proof tree that lifts the reductions into evaluation contexts, or Felleisen-style small-step semantics where the evaluation contexts are reified as plain old mathematical objects.

The benefit of the latter is that it requires no meta-mathematical reasoning--this is not to say it's impossible to use any of the others to prove soundness, but it perhaps requires less subtlety to write a proof about ordinary objects than one about proofs.

It reminds me of what Andrew Pitts has been saying for a while about his and Gabbay's denotational framework for theories of binding. They originally formulated their theory by working in a different set theory (one invented in the early 20th century by Fraenkel and Mostowski), but discovered that this required a certain "meta-logical sophistication" that made their work less accessible:

[Pitts and Gabbay [2002]] expresses its results in terms of an axiomatic set theory, based on the classical Fraenkel-Mostowski permutation model of set theory. In my experience, this formalism impedes the take up within computer science of the new ideas contained in that article. There is an essentially equivalent, but more concrete description of the model as standard sets equipped with some simple extra structure. These so-called nominal sets are introduced by Pitts [2003], and I will use them here to express α-structural recursion and induction within "ordinary mathematics"...

From "Alpha-structural recursion and induction", p. 462

Again, I think the moral of the story is that when you place all the objects you want to reason about at the object level, you avoid the need for meta-reasoning, which can make your proofs simpler and more accessible.

Sigfpe explains comonads

I just discovered this very cool discussion of comonads, which starts with a really lovely review of monads. The basic idea: monads allow you to compose two functions that inject their inputs into some "fancy structure." If we have functions f : a → m b and g : b → m c (i.e., Kleisli arrows), we can lift g to a function m b → m (m c) by the law that m is a functor, and then use the "flattening" monad law to unwrap the extra layer of structure on the result. As sigfpe (what is his/her real name?) puts it: "twice as fancy is still just fancy." I like that this provides an intuition for monads using the map/flatten formulation, as opposed to the usual unit/bind formulation, while still preserving the notion of "plumbing."

As for comonads, I'm starting to see the duality: comonads allow us to take some things already inside some fancy structure and map them down to something outside of that structure. For functions (co-Kleisli arrows) f : m a → b and g : m b → c, we can map f to a function m (m a) → m b, compose this with g on one end and the comonad operation m a → m (m a) on the other to get a function m a → c.

I'm still working on understanding some of the applications.

Compiling to JavaScript

Treating JavaScript as a back-end for a compiler is becoming more and more popular. Here are some examples of compilers that already target JavaScript:

• Squeak Smalltalk
  
• Scheme
  
• NarrativeJS
  
• Links
  
• OpenLaszlo
  
• Lisp
  
• Java
  
• Java
  
• Java
  
• Cross-browser JavaScript
  
• C#
  
• Ruby
  

This has come up in some of the ECMA-TG1 discussions, and I think some of Edition 4 will help compiler writers, in particular proper tail calls. On the other hand, I'm not sure whether "compiling X to JavaScript" is always a priori a net gain.

Some of these compilers are more toys than anything else: people always get a kick out of translating idioms between languages. That's fun, if a little boring after a while. But a lot of these tools are aiming at building abstractions for web programming, which is much more ambitious.

If you can properly build an abstraction on top of the many incompatibilities and low-level details of web platforms, then the abstraction is probably appropriate. But without a model for the "ideal" behavior of web browsers as approximated by each of the real ones, then the abstraction is likely to be either crippled or flawed. In this case, adding this layer of indirection may actually be maddeningly difficult to work with when it fails. If it's too simplistic, you'll eventually have to give up and drop down to the lower layer. This might be fine, if there are "trap doors" -- such as a foreign interface to JavaScript -- that allow the programmer to dip into the lower level when necessary. But if the abstractions have flaws in them, debugging will have become worse than before, because it involves debugging through the extra level of abstraction, wading through generated code, understanding the compatibility layer, etc.

I still think these abstractions are an important goal, but the hard part isn't the compilers. It's understanding the models, i.e., the implicit specifications for web browsers. Apparently Ian Hickson has done a lot of great work compiling empirical data about the behavior of existing web browsers to infer the implicit specs for web standards. This kind of work is messy and tedious, but important.

You want REPL's? We got REPL's!

JavaScript programming desperately needs development tools. Luckily, it's got some.

• Stand-alone command-line JavaScript shell for any Unix, including cygwin
• Web application debugging environment for Firefox
• JavaScript debugger for Firefox
• Web-based JavaScript shell
  

It took me a long, long time to find a command-line shell I could build in Windows with nothing more than ./configure, make, make install.

A stack is a context zipper

An evaluation context is a tree, and the stack is a zipper representation of the tree, allowing the part that changes the most--the hole--to be updated in constant time. In a context-sensitive reduction semantics, which models control as a stack, the "focus-down" rules unzip the context all the way down to its redex.

One cool thing you can do with this is reconstruct the source program. Given an expression evaluation stack, first replace the hole with the current expression being evaluated, then zip the context back up, and voilà! the original source code. I'm doing this in my JavaScript stepper to provide an intuitive visualization of the evaluation context within each function activation.

The only catch is to handle cycles in the source code, either due to recursion or loops. I don't have to worry about recursion, because I'm only doing this for individual function activations. Loops shouldn't be too much trouble, since they never accumulate stack.

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.

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.

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.